The post has been translated automatically. Original language: Russian
Formal verification is useful only when its result can be accurately linked to the system being checked and, if necessary, rechecked. A simple message saying "verification was successful" is not enough for this.
If the result exists only inside the developer's tool, the external customer or auditor is forced to trust the developer himself, his environment, and the saved report. Therefore, in Sekura, the result of a formal verification is processed into a separate artifact — SJP, Sekura Justified Proof.
SJP is needed so that the verification result can be saved, transferred to another party, and verified independently of the initial development process.
Not a report, but an evidentiary artifact.
A regular test or verification report is most often intended for a human. It can specify the number of completed checks, the version of the program, the launch date, and the overall result.
SJP solves a different problem. It stores the data necessary not only to read the result, but also to verify the proof chain itself.
Simplistically, the difference can be represented as follows:
A regular report
Verification completed successfully
37 properties checked
No errors foundand:
SJP
which implementation was checked
, which contract was used
what mathematical obligations were tested?
which dependencies were involved
with which key the result was signed withTherefore, SJP is closer not to a PDF report, but to a portable technical object that preserves the context of the completed check.
How does SJP appear
Verification does not start with SJP. First, there is an implementation and a formal description of the required properties.
For Sekura JS or the supported SystemVerilog, the general path can be represented as follows:
Realization
+
SJV
│
▼
The Verifier
│
▼
Mathematical obligations
│
▼
SMT solver
│
▼
SJPSJV describes what needs to be proved. The verifier converts the code and the contract into mathematical terms. The solver checks these conditions, after which the result is recorded in SJP.
Thus, SJP appears after the verification is performed and refers to a specific set of input data.
Why is the "successful" status alone not enough?
Suppose a developer reports:
Version 2.4 has passed formal verification.
Several questions arise at once. Which version 2.4 build was tested? Which contract was used? Were the dependencies the same? Has one of the input files changed after verification?
If there are no answers, the statement is difficult to verify.
Therefore, the evidence artifact must relate the result to specific inputs. Cryptographic hashes and other content identifiers are used for this purpose.
The meaning is simple:
implementation.bin
│
hash
│
▼
SJPIf the implementation changes even slightly, its hash will also change. The old SJP can no longer be considered proof for the new version without additional verification.
What is stored in SJP
The specific format is determined by the specification, but the meaning of the basic data is clear even without knowing the internal structure of the file.
The SJP should contain information that makes it possible to understand:
- what exactly was checked;
- which contract was used;
- what mathematical obligations were formed;
- what results did the solvers get?;
- what other evidence does the current result depend on?;
- which hashes are linked to the verification components?;
- which signature protects the package itself.
It is important that all these elements belong to the same evidence chain. It is not enough to keep a mathematical formula separate from the information about where it came from.
Mathematical obligations
The central part of the formal verification is the mathematical obligations.
For example, if the contract states that the value of the counter never exceeds a certain limit, the verifier must transform this statement and the behavior of the program into a task that the SMT solver can verify.
Conditional:
program behavior
+
formal property
A mathematical commitment
│
▼
unsatIn problems of this type, an unsat result may mean that a counterexample violating a given property does not exist within the framework of the constructed model.
For a human, this is no longer just a "property passed" string. There is a specific mathematical statement that can be passed to another solver.
Why keep obligations inside an evidence package
If the SJP retains the mathematical obligations themselves, the recipient does not necessarily have to fully trust the initial launch of the verifier.
He can repeat the check.
For example:
┌──► Z3
SJP ──► SMT ─────┤
└──► cvc5This approach is especially useful when evidence is shared between independent organizations.
The recipient can use the same solver or, if the commitment is compatible, a different solver. At the same time, it is important to understand the boundary of such verification: the repeated solution of the SMT problem confirms the mathematical result for the saved commitment, but by itself does not prove the correctness of all previous transformations.
Hashes connect the parts of the proof
SJP should be related not only to the original implementation, but also to other essential inputs.
For example:
implementation ───── hash ──
│
SJV ──────────── hash ──┼──► SJP
, dependencies ──── hash ──This approach allows you to detect the substitution of inputs after checking.
If the developer has changed the contract, implementation, or dependency, the old hashes will no longer match the new content. This is especially important for long-lived projects where the code is constantly changing.
The signature protects the evidence package itself
SJP can be digitally signed.
Sekura uses Ed25519 for this purpose. The signature allows you to verify that a specific package was signed by the owner of the corresponding private key and was not changed imperceptibly after signing.
But it is important to separate two different issues here.
The first:
Is the signature valid for this package?
This is a technical check.
Second:
Why do we trust the owner of this key?
This is already a matter of relations between organizations.
Sekura should not turn into a key certification authority. Trust in a particular public key can be established by a contract, internal company policy, direct key transfer, or other procedure.
SJP is not a certificate of absolute correctness
The name "proof" is easily misunderstood too broadly. Therefore, it is important to establish the boundary immediately.
SJP does not mean:
This program is correct in every possible sense.
It means that a specific formal verification of certain properties has been performed for a specific implementation within a given model.
If SJV contains only one property, a successful SJP confirms the verification of this property, rather than all possible program characteristics.
If the model does not take into account a certain external effect, SJP itself will not add it automatically.
Therefore, using SJP correctly requires looking at three things at the same time.:
What was checked?
On which implementation?
Under what assumptions?Without these questions, it is easy to interpret an evidentiary artifact more broadly than it allows.
Dependencies can also have their own sjps.
Large programs and hardware systems consist of components. Checking them as one giant object is not always convenient or even possible.
Therefore, proofs can be constructed compositionally.
Let's say module A uses modules B and C. If B and C already have proven contracts, A's verification can rely on these results.
Then the structure is obtained:
SJP-B ──┐
├──► SJP-A
SJP-C ──┘SJP-A fixes dependencies on specific SJP-B and SJP-C.
If B is changed and a new evidence package appears for it, it is already a different object. This model allows you to build a graph of evidence, where each level is precisely related to the previous one.
Why is this especially important for closed systems?
SJP becomes especially useful when the source code cannot be shared with another party.
In a normal situation, the customer can ask for the source code and conduct their own audit. This may not be possible for a commercial library, a closed hardware unit, or industrial software.
Then you can split the data.:
From the developer:
source code
build tools
internal environment
Transmitted:
SJV
SJP
public key
public format specificationThe recipient does not receive an implementation algorithm, but receives information about verified properties and a result that can be technically investigated.
This is not a substitute for auditing the source code in all cases. But where the sources cannot be disclosed, an additional level of verifiability appears.
SJP as a long-lived engineering artifact
There is another important application of SJP that is not directly related to the transfer to an external customer.
The project has been changing for years. Developers are leaving, tool versions are being updated, and the source code is being rewritten. After a few years, a simple text report "verified successfully" may almost lose its meaning.
SJP retains significantly more context.
It is possible to determine which implementation the proof referred to, which contract was used, which mathematical obligations were verified, and on which evidence the result depended.
Therefore, SJP is useful not only as a means of transferring evidence between companies, but also as part of the engineering history of the project itself.
How does SJP differ from tests?
Tests and formal proofs answer different questions.
The test shows:
We ran the program
on these inputs
and got this resultFormal verification seeks to establish:
For all the states
that are included in the model under consideration,
the specified property is not violated.Therefore, SJP is not a substitute for tests. Testing is still necessary to verify integration, hardware, performance, user behavior, and many other aspects.
But the test report and the SJP are of a different nature. The first captures the observed executions, the second is the result of checking formally defined properties.
Is it possible to check SJP after many years
This is why the portable format is especially useful.
If sufficient data is stored inside the package for re-verification and the format is publicly described, the proof does not have to remain linked to one workstation or one copy of the verifier.
The recipient can save the SJP along with the project documentation and later re-verify its integrity, signature, and mathematical obligations.
Of course, for really long-term verifiability, it is important to maintain format versions and compatibility rules. Therefore, the SJP specification must be versioned, and format changes must be explicitly documented.
From the launch result to the object that can be passed
The main purpose of SJP can be expressed very simply.
Without an evidence package, the process ends inside the developer's machine.:
code → verification → "successful"With SJP, the result becomes a separate object.:
code → verification → SJP → storage → transfer → re-verificationThis fundamentally changes the role of formal verification.
It ceases to be just an internal stage of development and becomes a source of technical evidence that can be included in a supply, audit, contractual relationship, or long-term project history.
SJV defines what needs to be proved. The verifier performs the verification. SJP saves and transfers its result.
Documentation
The verification language is SJV.
A supported subset of SystemVerilog.
The SJP specification, validation rules, version compatibility, and examples are available in the Sekura JS documentation section.
Формальная верификация полезна только тогда, когда её результат можно точно связать с проверяемой системой и при необходимости перепроверить. Простого сообщения «проверка прошла успешно» для этого недостаточно.
Если результат существует только внутри инструмента разработчика, внешний заказчик или аудитор вынужден доверять самому разработчику, его среде и сохранённому отчёту. Поэтому в Sekura результат формальной проверки оформляется в отдельный артефакт — SJP, Sekura Justified Proof.
SJP нужен для того, чтобы результат проверки можно было сохранить, передать другой стороне и проверить независимо от исходного процесса разработки.
Не отчёт, а доказательный артефакт
Обычный отчёт о тестировании или верификации чаще всего предназначен для человека. В нём может быть указано количество пройденных проверок, версия программы, дата запуска и общий результат.
SJP решает другую задачу. Он хранит данные, необходимые не только для чтения результата, но и для проверки самой доказательной цепочки.
Упрощённо разницу можно представить так:
Обычный отчёт
Проверка завершена успешно
37 свойств проверено
Ошибок не найденои:
SJP
какая реализация проверялась
какой контракт использовался
какие математические обязательства проверялись
какие зависимости участвовали
каким ключом подписан результатПоэтому SJP ближе не к PDF-отчёту, а к переносимому техническому объекту, который сохраняет контекст выполненной проверки.
Как появляется SJP
Проверка начинается не с SJP. Сначала есть реализация и формальное описание требуемых свойств.
Для Sekura JS или поддерживаемого SystemVerilog общий путь можно представить так:
Реализация
+
SJV
│
▼
Верификатор
│
▼
Математические обязательства
│
▼
SMT-решатель
│
▼
SJPSJV описывает, что требуется доказать. Верификатор преобразует код и контракт в математические условия. Решатель проверяет эти условия, после чего результат фиксируется в SJP.
Таким образом, SJP появляется уже после выполнения проверки и относится к конкретному набору входных данных.
Почему одного статуса «успешно» недостаточно
Предположим, разработчик сообщает:
Версия 2.4 прошла формальную верификацию.
Возникает сразу несколько вопросов. Какая именно сборка версии 2.4 проверялась? Какой контракт использовался? Были ли зависимости теми же? Не изменился ли один из входных файлов после проверки?
Если ответов нет, утверждение трудно проверять.
Поэтому доказательный артефакт должен связывать результат с конкретными входами. Для этого используются криптографические хеши и другие идентификаторы содержимого.
Смысл простой:
implementation.bin
│
hash
│
▼
SJPЕсли реализация изменится даже незначительно, изменится и её хеш. Старый SJP уже нельзя считать доказательством для новой версии без дополнительной проверки.
Что хранится в SJP
Конкретный формат определяется спецификацией, но смысл основных данных понятен даже без знания внутренней структуры файла.
В SJP должны быть зафиксированы сведения, позволяющие понять:
- что именно проверялось;
- какой контракт использовался;
- какие математические обязательства были сформированы;
- какие результаты получили решатели;
- от каких других доказательств зависит текущий результат;
- какими хешами связаны компоненты проверки;
- какой подписью защищён сам пакет.
Важно, что все эти элементы относятся к одной доказательной цепочке. Недостаточно хранить математическую формулу отдельно от информации о том, откуда она появилась.
Математические обязательства
Центральная часть формальной проверки — математические обязательства.
Например, если контракт утверждает, что значение счётчика никогда не превышает определённый предел, верификатор должен преобразовать это утверждение и поведение программы в задачу, которую способен проверить SMT-решатель.
Условно:
поведение программы
+
формальное свойство
│
▼
математическое обязательство
│
▼
unsatВ задачах такого типа результат unsat может означать, что контрпример, нарушающий заданное свойство, в рамках построенной модели не существует.
Для человека это уже не просто строка «property passed». Есть конкретное математическое утверждение, которое можно передать другому решателю.
Зачем хранить обязательства внутри доказательного пакета
Если SJP сохраняет сами математические обязательства, получателю не обязательно полностью доверять первоначальному запуску верификатора.
Он может повторить проверку.
Например:
┌──► Z3
SJP ──► SMT ─────┤
└──► cvc5Такой подход особенно полезен, когда доказательство передаётся между независимыми организациями.
Получатель может использовать тот же решатель или, если обязательство совместимо, другой решатель. При этом важно понимать границу такой проверки: повторное решение SMT-задачи подтверждает математический результат для сохранённого обязательства, но само по себе не доказывает корректность всех предыдущих преобразований.
Хеши связывают части доказательства
SJP должен быть связан не только с исходной реализацией, но и с другими существенными входами.
Например:
реализация ───── hash ──┐
│
SJV ──────────── hash ──┼──► SJP
│
зависимости ──── hash ──┘Такой подход позволяет обнаружить подмену входов после выполнения проверки.
Если разработчик изменил контракт, реализацию или зависимость, старые хеши уже не совпадут с новым содержимым. Это особенно важно для долгоживущих проектов, где код постоянно меняется.
Подпись защищает сам доказательный пакет
SJP может быть подписан цифровой подписью.
В Sekura для этого используется Ed25519. Подпись позволяет проверить, что конкретный пакет был подписан владельцем соответствующего закрытого ключа и после подписания не был изменён незаметно.
Но здесь важно разделять два разных вопроса.
Первый:
Действительна ли подпись для этого пакета?
Это техническая проверка.
Второй:
Почему мы доверяем владельцу этого ключа?
Это уже вопрос отношений между организациями.
Sekura не должна превращаться в центр сертификации ключей. Доверие к конкретному открытому ключу может быть установлено договором, внутренней политикой компании, прямой передачей ключа или другой процедурой.
SJP не является сертификатом абсолютной правильности
Название «proof» легко понять слишком широко. Поэтому важно сразу установить границу.
SJP не означает:
Эта программа правильна во всех возможных смыслах.
Он означает, что была выполнена конкретная формальная проверка определённых свойств для определённой реализации в рамках заданной модели.
Если SJV содержит только одно свойство, успешный SJP подтверждает проверку этого свойства, а не всех возможных характеристик программы.
Если модель не учитывает определённый внешний эффект, сам SJP не добавит его автоматически.
Поэтому корректное использование SJP требует одновременно смотреть на три вещи:
Что проверялось?
На какой реализации?
При каких предположениях?Без этих вопросов доказательный артефакт легко интерпретировать шире, чем он позволяет.
Зависимости тоже могут иметь собственные SJP
Большие программы и аппаратные системы состоят из компонентов. Проверять их как один гигантский объект не всегда удобно или вообще возможно.
Поэтому доказательства могут строиться композиционно.
Допустим, модуль A использует модули B и C. Если B и C уже имеют доказанные контракты, проверка A может опираться на эти результаты.
Тогда получается структура:
SJP-B ──┐
├──► SJP-A
SJP-C ──┘В SJP-A фиксируются зависимости от конкретных SJP-B и SJP-C.
Если B будет изменён и для него появится новый доказательный пакет, это уже другой объект. Такая модель позволяет строить граф доказательств, где каждый уровень точно связан с предыдущим.
Почему это особенно важно для закрытых систем
SJP становится особенно полезным, когда исходный код нельзя передавать другой стороне.
В обычной ситуации заказчик может попросить исходники и провести собственный аудит. Для коммерческой библиотеки, закрытого аппаратного блока или промышленного программного обеспечения это может быть невозможно.
Тогда можно разделить данные:
У разработчика:
исходный код
инструменты сборки
внутренняя среда
Передаются:
SJV
SJP
открытый ключ
публичная спецификация форматаПолучатель не получает алгоритм реализации, но получает сведения о проверенных свойствах и результат, который можно технически исследовать.
Это не заменяет аудит исходного кода во всех случаях. Но там, где исходники раскрывать нельзя, появляется дополнительный уровень проверяемости.
SJP как долгоживущий инженерный артефакт
Есть ещё одно важное применение SJP, не связанное напрямую с передачей внешнему заказчику.
Проект меняется годами. Разработчики уходят, версии инструментов обновляются, исходный код переписывается. Через несколько лет простой текстовый отчёт «проверено успешно» может практически потерять смысл.
SJP сохраняет значительно больше контекста.
Можно определить, к какой реализации относилось доказательство, какой контракт использовался, какие математические обязательства проверялись и от каких доказательств зависел результат.
Поэтому SJP полезен не только как средство передачи доказательства между компаниями, но и как часть инженерной истории самого проекта.
Чем SJP отличается от тестов
Тесты и формальные доказательства отвечают на разные вопросы.
Тест показывает:
Мы запустили программу
на этих входных данных
и получили такой результатФормальная проверка стремится установить:
При всех состояниях,
которые входят в рассматриваемую модель,
заданное свойство не нарушаетсяПоэтому SJP не является заменой тестам. Тестирование по-прежнему необходимо для проверки интеграции, оборудования, производительности, пользовательского поведения и множества других аспектов.
Но тестовый отчёт и SJP имеют разную природу. Первый фиксирует наблюдавшиеся выполнения, второй — результат проверки формально заданных свойств.
Можно ли проверить SJP через много лет
Именно для этого переносимый формат особенно полезен.
Если внутри пакета сохранены достаточные данные для повторной проверки и формат публично описан, доказательство не обязано оставаться привязанным к одной рабочей станции или одной копии верификатора.
Получатель может сохранить SJP вместе с проектной документацией и позже снова проверить его целостность, подпись и математические обязательства.
Конечно, для действительно долгосрочной проверяемости важно сохранять версии форматов и правила совместимости. Поэтому спецификация SJP должна быть версионируемой, а изменения формата — явно документироваться.
От результата запуска к объекту, который можно передать
Главное назначение SJP можно выразить очень просто.
Без доказательного пакета процесс заканчивается внутри машины разработчика:
код → проверка → «успешно»С SJP результат становится отдельным объектом:
код → проверка → SJP → хранение → передача → повторная проверкаЭто принципиально меняет роль формальной верификации.
Она перестаёт быть только внутренним этапом разработки и становится источником технического доказательства, которое можно включить в поставку, аудит, договорные отношения или долговременную историю проекта.
SJV определяет, что требуется доказать. Верификатор выполняет проверку. SJP сохраняет и переносит её результат.
Документация
Поддерживаемое подмножество SystemVerilog.
Спецификация SJP, правила проверки, совместимость версий и примеры доступны в разделе документации Sekura JS.
Share
