Поскольку наши личные данные все чаще используются во многих приложениях, от рекламы до финансов и здравоохранения, защита конфиденциальной информации стала важной функцией вычислительных архитектур. Приложения, обрабатывающие такие данные, должны доверять системному программному обеспечению, на которое они полагаются, такому как операционные системы и гипервизоры, но такое системное программное обеспечение является сложным и часто имеет уязвимости, которые могут поставить под угрозу конфиденциальность и целостность данных.

В течение последних двух лет исследователи из Columbia Engineering работали с Arm, ведущей компанией по разработке полупроводниковой интеллектуальной собственности и программного обеспечения , над устранением этих уязвимостей. Теперь команда представила ключевые технологии проверки для Arm Confidential Compute Architecture (Arm CCA), новой функции архитектуры Armv9-A. Документ, представленный 12 июля на 16-м симпозиуме USENIX по проектированию и внедрению операционных систем (OSDI ’22) в Карлсбаде, Калифорния, демонстрирует первую формальную проверку прототипа прошивки Arm CCA .

Arm CCA полагается на прошивку для управления аппаратным обеспечением для обеспечения гарантий безопасности, поэтому очень важно, чтобы прошивка была правильной и безопасной. Хотя многие предыдущие системы полагаются на прошивку, ни одна из них не может гарантировать, что прошивка не содержит ошибок. Формальная верификация — это относительно новая методология, которая в настоящее время используется для гарантии правильности программного/аппаратного обеспечения. Вместо тестирования формальная верификация использует математические модели, чтобы доказать, что программное и аппаратное обеспечение абсолютно корректны, и, таким образом, обеспечивает наивысший уровень гарантии правильности.

«Мы впервые доказали, что прошивка правильная и безопасная, что привело к первой демонстрации архитектуры конфиденциальных вычислений, поддерживаемой официально проверенной прошивкой», — сказал ведущий автор исследования Сюпэн Ли, доктор философии. студент Ронхуэй Гу, доцент кафедры компьютерных наук семьи Тан, и Джейсон Ни, профессор компьютерных наук и содиректор Лаборатории программных систем.

Хотя существует множество подходов к проверке правильности простых программ, они не подходят для чего-то столь сложного, как прошивка CCA, поэтому исследователям пришлось разработать новые методы проверки, чтобы сделать возможной проверку прошивки Arm CCA. Например, прошивка CCA разработана для обеспечения масштабируемости и производительности, поэтому она допускает параллельную работу в высокой степени и сочетает в себе код C и ассемблера. Параллельная работа стала возможной благодаря использованию методов мелкозернистой синхронизации и кода с гонками данных.

Принцип разработки Arm CCA заключается в том, что ненадежное программное обеспечение должно сохранять контроль над управлением аппаратными ресурсами, поэтому ключевой задачей является доказательство того, что система по-прежнему безопасна, даже если ненадежное программное обеспечение может забирать аппаратные ресурсы по своему усмотрению. Предыдущие подходы не позволяли проверять программы с такими свойствами. Этот новый метод проверки достаточно мощен, чтобы проверять параллельную прошивку как с кодом C, так и с ассемблерным кодом.

«Ошибки действительно трудно найти с помощью классических методов тестирования программного обеспечения», — сказал Сюхэн Ли, еще один доктор философии. ученик Ние и Гу, соавтор работы. «Таким образом, мы продемонстрировали важность и ценность наших формальных методов проверки, и конечным результатом стала первая демонстрация конфиденциальной вычислительной архитектуры, поддерживаемой проверенной прошивкой».

Команда очень взволнована новыми технологиями проверки, которые можно использовать для подтверждения правильности реализаций прошивки, лежащей в основе Arm CCA. Процессоры Arm уже развернуты на миллиардах устройств по всему миру. Поскольку Arm CCA все чаще используется для защиты личных данных пользователей, особенно в облачных службах и за ее пределами, методы проверки, продемонстрированные в этом документе, обеспечат значительное улучшение защиты и безопасности данных.

Одной из проблем, связанных с формальными методологиями, применяемыми к программному обеспечению, является необходимость адаптации доказательств при обновлении программного обеспечения. Исследователи работают над новыми технологиями, которые помогут им поэтапно и быстро проверять обновления прошивки Arm CCA и обеспечивать постоянную проверку последней доступной прошивки.

Гу и Нье добавили, что они «увидели мощь и потенциал формальной проверки в нашей работе, и мы убеждены, что формальная проверка является важным методом, который в ближайшем будущем заменит тестирование программного обеспечения в настоящее время».