The post has been translated automatically. Original language: Russian
Jupiter Soft has developed a working set of tools for compiling and formally verifying programs in the Sekura JS language.
The main idea of the project is to check not only the source code, but also the actually compiled program.
The chain looks like this:
Sekura JS
↓
compilation
↓
SOBJ
↓
symbolic execution
↓
checking SJV-contract
↓
Z3
↓
the result of verificationWhy do we need such a check?
The usual tests check individual scenarios of the program.
For example, you can check that when the counter value is 10, the function increases it to 11.
Formal verification solves another problem: it checks a property for all valid values and states described in the contract at once.
The SJV specification language, Sekura Justified Verification, is used for this purpose.
For example, the requirement:
function increment {
counter' = counter + 1;
}this means that after the function is fully executed, the new counter value must be equal to the old value plus one.
The compiled program is checked
One of the key features of the system is that the check is performed relative to SOBJ, that is, the result of the Sekura JS compilation.
This allows you to take into account not only the errors of the program itself, but also possible compiler errors.
During development, the verifier has already helped to detect a real compiler error: in one case, the global value u32 was mistakenly interpreted as a pointer, which is why the arithmetic operation was performed incorrectly.
The error has been found and fixed.
How the proof works
The system performs symbolic execution of the program and builds a mathematical condition describing a possible violation of the contract.
This condition is passed to the SMT solver Z3.
If Z3 finds a possible violation, the system returns a specific counterexample.
If Z3 proves that the violation is impossible, the result is:
UNSATThat is, within a given contract and environment, there is no acceptable condition in which a program violates a verifiable requirement.
What has already been implemented
The current version works:
- checking SJV contracts;
- symbolic execution of SOBJ;
- integration with Z3;
- checking memory boundaries and alignment;
- checking the stack;
- the static MMU model;
- ABI retention control;
- derivation of specific counterexamples;
- generating the SJP report;
- support for Sekura JS and SJV files in Visual Studio Code.
Not only a minimal example has been created for verification, but also a more complex scenario containing 6 states and 10 functions, transitions between modes, global variables and arithmetic operations.
The last general run of the project ended with the result:
41 / 41 tests passedWhat does VERIFIED mean?
Formal verification does not mean that the program is automatically proven correct under any possible conditions.
The proof refers to:
- a specific version of the program;
- a specific SJV specification;
- the specified environment;
- supported execution model;
- the declared amount of verification.
If an important requirement is not described in the specification, it is not automatically considered proven.
The next stage
The main circuit is already working now.:
SJS
→ SOBJ
→ symbolic execution
→ SJV
→ Z3
→ SAT / UNSAT
→ SJPFurther work will be related to the expansion of support for optimized code, dynamic MMU, more complex cycles, and the development of independent, verifiable, evidence-based certificates.
Result
Sekura JS combines system programming and formal verification in a single development process.
The developer can:
describe the requirements
↓
write the program
↓
compile it
↓
check the compiled implementation
↓
get a proof or a specific counterexampleThe aim of the project is to make formal methods a practical tool for system software development, rather than a separate research procedure.
В Jupiter Soft разработан рабочий набор инструментов для компиляции и формальной проверки программ на языке Sekura JS.
Основная идея проекта — проверять не только исходный код, но и фактически скомпилированную программу.
Цепочка выглядит так:
Sekura JS
↓
компиляция
↓
SOBJ
↓
символическое исполнение
↓
проверка по SJV-контракту
↓
Z3
↓
результат верификацииЗачем нужна такая проверка
Обычные тесты проверяют отдельные сценарии работы программы.
Например, можно проверить, что при значении счётчика 10 функция увеличивает его до 11.
Формальная верификация решает другую задачу: она проверяет свойство сразу для всех допустимых значений и состояний, описанных в контракте.
Для этого используется язык спецификаций SJV — Sekura Justified Verification.
Например, требование:
function increment {
counter' = counter + 1;
}означает, что после полного выполнения функции новое значение counter должно быть равно старому значению плюс один.
Проверяется скомпилированная программа
Одна из ключевых особенностей системы — проверка выполняется относительно SOBJ, то есть результата компиляции Sekura JS.
Это позволяет учитывать не только ошибки самой программы, но и возможные ошибки компилятора.
Во время разработки верификатор уже помог обнаружить реальную ошибку компилятора: глобальное значение u32 в одном из случаев ошибочно интерпретировалось как указатель, из-за чего арифметическая операция выполнялась неправильно.
Ошибка была найдена и исправлена.
Как работает доказательство
Система выполняет символическое исполнение программы и строит математическое условие, описывающее возможное нарушение контракта.
Это условие передаётся SMT-решателю Z3.
Если Z3 находит возможное нарушение, система возвращает конкретный контрпример.
Если Z3 доказывает, что нарушение невозможно, результатом становится:
UNSATТо есть в пределах заданного контракта и окружения не существует допустимого состояния, при котором программа нарушает проверяемое требование.
Что уже реализовано
В текущей версии работают:
- проверка SJV-контрактов;
- символическое исполнение SOBJ;
- интеграция с Z3;
- проверка границ и выравнивания памяти;
- проверка стека;
- статическая модель MMU;
- контроль сохранения ABI;
- вывод конкретных контрпримеров;
- формирование отчёта SJP;
- поддержка файлов Sekura JS и SJV в Visual Studio Code.
Для проверки создан не только минимальный пример, но и более сложный сценарий, содержащий 6 состояний и 10 функций, переходы между режимами, глобальные переменные и арифметические операции.
Последний общий прогон проекта завершился результатом:
41 / 41 tests passedЧто означает VERIFIED
Формальная верификация не означает, что программа автоматически доказана правильной при любых возможных условиях.
Доказательство относится к:
- конкретной версии программы;
- конкретной SJV-спецификации;
- заданному окружению;
- поддерживаемой модели выполнения;
- заявленному объёму проверки.
Если важное требование не описано в спецификации, оно не считается автоматически доказанным.
Следующий этап
Сейчас основной контур уже работает:
SJS
→ SOBJ
→ symbolic execution
→ SJV
→ Z3
→ SAT / UNSAT
→ SJPДальнейшая работа будет связана с расширением поддержки оптимизированного кода, динамической MMU, более сложных циклов и развитием независимых проверяемых доказательных сертификатов.
Итог
Sekura JS объединяет системное программирование и формальную верификацию в одном процессе разработки.
Разработчик может:
описать требования
↓
написать программу
↓
скомпилировать её
↓
проверить скомпилированную реализацию
↓
получить доказательство или конкретный контрпримерЦель проекта — сделать формальные методы практическим инструментом разработки системного программного обеспечения, а не отдельной исследовательской процедурой.
Share
