The post has been translated automatically. Original language: Russian
Formal verification is valuable only when it is possible to establish exactly what was tested and under what conditions the result was obtained. A simple success message is not enough.
In a few months, the program may change, the compiler may receive a new version, and the verification tool may have additional features. If the original data and information about the tools were not saved along with the result, it becomes difficult to understand which version of the system the performed check belonged to.
Therefore, at Sekura, we consider reproducibility as an essential part of evidence-based work.
Why is one result not enough
Imagine that the developer has completed a formal verification of the program and saved a message about the successful result.
By itself, it says almost nothing about checking after a while. You need to know which version of the source program was used, which machine code the compiler created, which formal requirement was checked, and which versions of the tools produced the result.
If at least one of these elements has changed, the previous result can no longer be automatically attributed to the new version.
Therefore, along with the result, it is necessary to save the entire chain of source data.
What is associated with the verification result?
When testing a program for Sekura JS, several basic elements are involved.
There is a source program. The compiler creates a machine object for the Memora8 architecture from it. The formal requirement that this machine code must meet is set separately.
After that, the SJV tool performs a check and generates the result.
For an evidence base, it is important to preserve the exact contents of each of these elements, as well as the versions of the compiler and the verification tool.
This way, you can establish not just the fact of a successful launch, but the exact configuration for which the result was obtained.
Why do we need checksums?
The file name does not allow you to reliably determine its contents.
For example, the file may still have the same name, even though there is already a new version of the program inside. Therefore, SHA-256 checksums are calculated for verification-related data.
The checksum allows you to detect changes in the file contents. Even a small change results in a different value.
To verify Sekura JS, such values can be fixed for the source program, the formal description, the machine object, the verification result, and the executable tools used.
This allows you to determine exactly which data was involved in a particular check.
SJP Package
After formal verification, the result can be saved in the SJP package.
His task is to collect in one place the information necessary for the subsequent verification of the result. The package is associated with a specific implementation and a specific formal requirement.
It can also store mathematical problems that were generated by SJV during verification.
This allows you to store not only the final message, but also the data on the basis of which the mathematical solver came to its result.
Such a package becomes much more useful than a regular text report.
Repeated verification
The saved SJP can be checked again.
In this case, the integrity of the associated data is first monitored. Then the saved mathematical problems are transferred back to the solver.
If the contents of the package have been changed, the checksums will no longer match. If everything remains unchanged, mathematical problems can be solved anew and the result can be compared with the saved one.
Thus, the proof does not end at the time of the initial launch. You can check it again later.
Why do we use two solvers?
The main mathematical solver in our current chain is Z3.
For additional verification, the same mathematical problems can be transferred to another independent solver, CVC5.
If both tools produce the same definite result, this reduces the dependence on the possible error of one particular solver.
But here it is important to correctly understand the boundary of such confirmation. The coincidence of the results means that two different tools solved the same mathematical problem in the same way.
This does not automatically prove that all the previous steps are correct.
Where does trust remain
Before a mathematical problem gets into Z3 or CVC5, it needs to be constructed.
The source program first goes through the compiler. SJV then analyzes the resulting machine code, links it to the formal requirement, and forms a mathematical representation of the verification.
Therefore, even the coincidence of the results of the two solvers does not answer a separate question: whether SJV correctly transformed the behavior of the machine code into a mathematical model.
This boundary must remain explicit.
Reproducibility does not mean that the entire tool chain is automatically proven. It allows you to determine exactly what has been retested and which components are still in the trusted part of the system.
Why is the compiler version important?
The same source program does not necessarily produce the same machine code in different versions of the compiler.
Optimization, the placement of values in registers, the choice of instructions, or other part of code generation may change.
Therefore, the result of a formal check should be related to a specific version of the compiler.
For the next version, the source program can be compiled anew, get a new machine object, and repeat the same check.
If the formal requirement remains the same, it becomes possible to check whether the required behavior has been preserved after the compiler has been changed.
Why is the version of the verification tool important?
The formal verification tool itself is also evolving.
An error may be fixed, a new machine instruction may be added, the memory representation may be changed, or the scope of supported programs may be expanded.
Therefore, it is necessary to know not only the compiler version, but also the exact SJV version that produced the result.
So the evidentiary record refers to a certain state of the entire verification chain.
If important components are changed, the check can be repeated with a new set of tools.
Signature of the result
The evidence package can be signed with an electronic signature used inside the system.
Such a signature alone does not prove the correctness of the program. Its purpose is different — to confirm the integrity of the committed package and to detect its subsequent modification.
The public part of the key is sufficient for the verifying party. The closed part remains with the owner who created the package.
Together with the checksums, this allows you to establish that it is the data set that was originally recorded that is being checked.
What happens after changing the program
After successful verification, development usually continues.
The program is changing, errors are being fixed, and new features are being added. The old result does not need to be deleted.
It remains a proof of a property of the previous version.
For the new version, a new compilation and a new formal verification are performed. After it, a new evidence package is created.
This is how the project history is gradually formed, in which you can see which property has been confirmed for each specific version.
Why do I need an independent re-check?
The less a result depends on trust in its author, the higher its engineering value.
If another developer receives the source program, a formal description, a machine object, a proof package, and information about the tools, they can check the checksums and repeat the saved mathematical checks.
It doesn't have to be limited to the developer's statement that the check was once successfully completed.
He can independently verify that the saved data leads to the same result.
It is for this reason that the possibility of open publication of materials and their independent study is important for the Sekura evidence base.
Reproducibility as part of engineering proof
A regular report answers the question: what result was obtained at a certain moment.
class="paragraph"> The reproduced test answers a more meaningful question: is it possible to establish accurate baseline data and get the same result again?
For Sekura, this is a fundamental difference.
The evidence base should include not only the verification result, but also the source program, the machine result of compilation, the formal requirement, tool versions, checksums, and the saved verification package.
Then, instead of saying "we have tested this program," we can make a much more accurate statement.: for this particular version of the program, this machine code, and this formal requirement, there is a stored result that can be checked repeatedly.
It is precisely this reproducibility that we consider to be a necessary part of formal verification.
Формальная проверка имеет ценность только тогда, когда можно точно установить, что именно проверялось и при каких условиях был получен результат. Простого сообщения об успешном завершении недостаточно.
Через несколько месяцев программа может измениться, компилятор получить новую версию, а средство проверки — дополнительные возможности. Если вместе с результатом не были сохранены исходные данные и сведения об инструментах, становится трудно понять, к какой версии системы относилась выполненная проверка.
Поэтому в Sekura мы рассматриваем воспроизводимость как обязательную часть доказательной работы.
Почему одного результата недостаточно
Представим, что разработчик выполнил формальную проверку программы и сохранил сообщение об успешном результате.
Само по себе оно почти ничего не говорит о проверке спустя некоторое время. Нужно знать, какая версия исходной программы использовалась, какой машинный код создал компилятор, какое формальное требование проверялось и какими версиями инструментов был получен результат.
Если хотя бы один из этих элементов изменился, прежний результат уже нельзя автоматически относить к новой версии.
Поэтому вместе с итогом необходимо сохранять всю цепочку исходных данных.
Что связывается с результатом проверки
При проверке программы на Sekura JS участвуют несколько основных элементов.
Есть исходная программа. Компилятор создаёт из неё машинный объект для архитектуры Memora8. Отдельно задаётся формальное требование, которому должен соответствовать этот машинный код.
После этого средство SJV выполняет проверку и формирует результат.
Для доказательной базы важно сохранить точное содержимое каждого из этих элементов, а также версии компилятора и средства проверки.
Так можно установить не просто факт успешного запуска, а точную конфигурацию, для которой был получен результат.
Зачем нужны контрольные суммы
Имя файла не позволяет надёжно определить его содержимое.
Например, файл может по-прежнему называться одинаково, хотя внутри уже находится новая версия программы. Поэтому для связанных с проверкой данных рассчитываются контрольные суммы SHA-256.
Контрольная сумма позволяет обнаружить изменение содержимого файла. Даже небольшое изменение приводит к другому значению.
Для проверки Sekura JS такие значения могут фиксироваться для исходной программы, формального описания, машинного объекта, результата проверки и используемых исполняемых инструментов.
Благодаря этому можно точно определить, какие именно данные участвовали в конкретной проверке.
Пакет SJP
После формальной проверки результат можно сохранить в пакете SJP.
Его задача — собрать в одном месте сведения, необходимые для последующей проверки результата. Пакет связывается с конкретной реализацией и конкретным формальным требованием.
В нём также могут сохраняться математические задачи, которые были сформированы SJV во время проверки.
Это позволяет хранить не только итоговое сообщение, но и данные, на основании которых математический решатель пришёл к своему результату.
Такой пакет становится значительно полезнее обычного текстового отчёта.
Повторная проверка
Сохранённый SJP можно проверить повторно.
При этом сначала контролируется целостность связанных данных. Затем сохранённые математические задачи снова передаются решателю.
Если содержимое пакета было изменено, контрольные суммы перестанут совпадать. Если всё осталось неизменным, математические задачи можно решить заново и сравнить результат с сохранённым.
Таким образом, доказательство не заканчивается в момент первоначального запуска. Его можно проверить ещё раз позднее.
Почему мы используем два решателя
Основным математическим решателем в нашей текущей цепочке является Z3.
Для дополнительной проверки те же математические задачи можно передать другому независимому решателю — CVC5.
Если оба средства дают одинаковый определённый результат, это уменьшает зависимость от возможной ошибки одного конкретного решателя.
Но здесь важно правильно понимать границу такого подтверждения. Совпадение результатов означает, что два разных инструмента одинаково решили одну и ту же математическую задачу.
Это ещё не доказывает автоматически правильность всех предыдущих этапов.
Где остаётся доверие
До того как математическая задача попадает в Z3 или CVC5, её необходимо построить.
Исходная программа сначала проходит через компилятор. Затем SJV анализирует полученный машинный код, связывает его с формальным требованием и формирует математическое представление проверки.
Поэтому даже совпадение результатов двух решателей не отвечает на отдельный вопрос: правильно ли SJV преобразовал поведение машинного кода в математическую модель.
Эта граница должна оставаться явной.
Воспроизводимость не означает, что автоматически доказана вся цепочка инструментов. Она позволяет точно определить, что именно было повторно проверено и какие компоненты всё ещё находятся в доверенной части системы.
Почему важна версия компилятора
Одинаковая исходная программа не обязательно создаёт одинаковый машинный код в разных версиях компилятора.
Может измениться оптимизация, размещение значений по регистрам, выбор инструкций или другая часть генерации кода.
Поэтому результат формальной проверки должен быть связан с конкретной версией компилятора.
Для следующей версии исходную программу можно скомпилировать заново, получить новый машинный объект и повторить ту же проверку.
Если формальное требование осталось прежним, становится возможным проверить, сохранилось ли необходимое поведение после изменения компилятора.
Почему важна версия средства проверки
Само средство формальной проверки тоже развивается.
Может быть исправлена ошибка, добавлена новая машинная инструкция, изменено представление памяти или расширена область поддерживаемых программ.
Поэтому необходимо знать не только версию компилятора, но и точную версию SJV, которой был получен результат.
Так доказательная запись относится к определённому состоянию всей проверяющей цепочки.
При изменении важных компонентов проверку можно выполнить повторно уже новым набором инструментов.
Подпись результата
Доказательный пакет можно подписать электронной подписью, используемой внутри системы.
Такая подпись сама по себе не доказывает правильность программы. Её назначение другое — подтвердить целостность зафиксированного пакета и позволить обнаружить его последующее изменение.
Проверяющей стороне достаточно открытой части ключа. Закрытая часть остаётся у владельца, сформировавшего пакет.
Вместе с контрольными суммами это позволяет установить, что проверяется именно тот набор данных, который был первоначально зафиксирован.
Что происходит после изменения программы
После успешной проверки разработка обычно продолжается.
Программа меняется, исправляются ошибки, добавляются новые возможности. Старый результат при этом не нужно удалять.
Он остаётся доказательством свойства предыдущей версии.
Для новой версии выполняется новая компиляция и новая формальная проверка. После неё создаётся новый доказательный пакет.
Так постепенно формируется история проекта, в которой можно увидеть, какое свойство было подтверждено для каждой конкретной версии.
Зачем нужна независимая повторная проверка
Чем меньше результат зависит от доверия к его автору, тем выше его инженерная ценность.
Если другой разработчик получает исходную программу, формальное описание, машинный объект, доказательный пакет и сведения об инструментах, он может проверить контрольные суммы и повторить сохранённые математические проверки.
Ему не обязательно ограничиваться утверждением разработчика о том, что проверка когда-то была успешно выполнена.
Он может самостоятельно убедиться, что сохранённые данные приводят к тому же результату.
Именно по этой причине для доказательной базы Sekura важна возможность открытой публикации материалов и их независимого изучения.
Воспроизводимость как часть инженерного доказательства
Обычный отчёт отвечает на вопрос: какой результат был получен в определённый момент.
Воспроизводимая проверка отвечает на более содержательный вопрос: можно ли установить точные исходные данные и снова получить тот же результат.
Для Sekura это принципиальная разница.
Доказательная база должна включать не только итог проверки, но и исходную программу, машинный результат компиляции, формальное требование, версии инструментов, контрольные суммы и сохранённый пакет проверки.
Тогда вместо фразы «мы проверили эту программу» можно сделать значительно более точное утверждение: для этой конкретной версии программы, этого машинного кода и этого формального требования существует сохранённый результат, который можно проверить повторно.
Именно такую воспроизводимость мы считаем необходимой частью формальной проверки.
Share
