Новый инструмент автоматизирует формальную проверку системного программного обеспечения

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

Недавняя работа под руководством профессоров Ронхуэй Гу и Джейсона Ние представила новый инструмент Spoqчто значительно сокращает сложные усилия, которые люди должны прилагать для проверки реального программного обеспечения, и позволяет проверять существующий код систем C без изменений.

Формальная проверка предлагает систематический и строгий подход к проверке программного и аппаратного обеспечения, помогая гарантировать, что системы работают правильно и соответствуют заданным спецификациям. С помощью Spoq многие аспекты формальной проверки можно автоматизировать, что значительно сокращает усилия по проверке вручную. Документ был представлен на 17-й конференции USENIX по проектированию и внедрению операционных систем (OSDI) 12 июля 2023 года.

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

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

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

Исследование называется «Spoq: масштабирование машинно-проверяемой системы в Coq.”