Формальная проверка архитектуры секвестрированного шифрования

Технический документ под названием «Проверка безопасности архитектур с низким уровнем доверия» был опубликован исследователями из Принстонского университета, Мичиганского университета и колледжа Лафайет.

Абстрактные:

«Архитектуры с низким уровнем доверия работают, с точки зрения программного обеспечения, с всегда зашифрованными данными и значительно снижают уровень доверия к оборудованию до небольшого безпрограммного анклавного компонента. В этой статье мы проводим полную формальную проверку конкретной архитектуры с низким уровнем доверия, архитектуры секвестрированного шифрования (SE), чтобы показать, что конструкция защищена от прямого раскрытия данных и цифровых побочных каналов для всех возможных программ. Сначала мы определим требования безопасности ISA или SE архитектуры с низким уровнем доверия. Если посмотреть вверх, то этот ISA служит абстракцией аппаратного обеспечения для программного обеспечения и используется, чтобы показать, как любая программа, содержащая эти инструкции, не может утечь информацию, в том числе через цифровые побочные каналы. Если смотреть вниз, то этот ISA представляет собой спецификацию аппаратного обеспечения и используется для определения обязательств по доказательству для любой реализации RTL, вытекающих из требований безопасности уровня ISA. Они охватывают как функциональные, так и цифровые утечки побочного канала. Далее мы покажем, как эти обязательства по доказательству могут быть успешно выполнены с использованием коммерческих формальных инструментов проверки. Мы демонстрируем эффективность нашей методики проверки безопасности RTL для семи различных правильных и ошибочных реализаций архитектуры SE».

Найдите технический документ здесь. Опубликовано в сентябре 2023 г. (препринт).

Тан, Циньхан, Йонатан Фиссеха, Шибо Чен, Лорен Бернаки, Жан-Батист Жаннен, Шарад Малик и Тодд Остин. «Проверка безопасности архитектур с низким уровнем доверия». Препринт arXiv arXiv:2309.00181 (2023).

Связанные Чтение
Проверка и проверка безопасности
Функциональная проверка выходит за рамки ее возможностей для обеспечения безопасности и надежности систем. Новая поддержка исходит от аппаратного и программного обеспечения.
Новые концепции, необходимые для проверки безопасности
Почему так сложно убедиться, что оборудование работает правильно и способно обнаруживать уязвимости, которые могут проявиться в полевых условиях.

• SEO-контент и PR-распределение. Получите усиление сегодня.
• PlatoData.Network Вертикальный генеративный ИИ. Расширьте возможности себя. Доступ здесь.
• ПлатонАйСтрим. Интеллект Web3. Расширение знаний. Доступ здесь.
• ПлатонЭСГ. Автомобили / электромобили, Углерод, чистые технологии, Энергия, Окружающая среда, Солнечная, Управление отходами. Доступ здесь.
• ПлатонЗдоровье. Биотехнологии и клинические исследования. Доступ здесь.
• ЧартПрайм. Улучшите свою торговую игру с ChartPrime. Доступ здесь.
• Смещения блоков. Модернизация права собственности на экологические компенсации. Доступ здесь.
• Источник: https://semiengineering.com/formal-verification-of-a-sequestered-encryption-architecture/