The post has been translated automatically. Original language: Russian
The source code cannot always be transferred to the customer, partner, or auditor. It may contain trade secrets, the company's own algorithms, licensed components, or simply be part of a product that is delivered only in binary form.
At the same time, the other side may have a well-founded question.: why should we believe that this program really has the stated properties?
The usual answer is tests, reports, certificates, or source code audits. But there is another option: to formally describe the required properties of the program, mathematically verify them, and transmit the verification result separately from the source code.
This is where it becomes possible to separate the implementation, the requirements for it, and the proof.
It is not necessary to check "correctness at all".
The phrase "the program has been formally verified" in itself means almost nothing. Any check must have specific properties.
For example, the control module may require:
- the counter never goes beyond the allowed range;
- a certain state is unattainable;
- the operation does not change the protected memory area;
- after the function is executed, the specified condition is fulfilled.;
- The transition from one state to another is possible only with certain input data.
Formal verification does not answer the question.:
Is this program correct?
And for a more precise question:
Are the specified properties for this implementation fulfilled within the framework of the accepted model and the specified assumptions?
This is a fundamental difference. If a certain property has not been formulated, its absence among the errors does not mean that it has been proven.
The source code and the contract can be separated
Let's imagine a company that has developed a control module for industrial equipment. She does not want to transfer its source code to the customer, but the customer needs to make sure that the module complies with several critical rules.
The system can be divided into three parts:
Closed implementation
│
▼
A formal contract
│
▼
Verifiable proofThe implementation remains with the developer. A formal contract describes the properties that must be fulfilled. The verification results in a separate evidentiary artifact.
In Sekura, SJV and SJP are used for these last two parts.
SJV describes exactly what needs to be proved
SJV is a language for describing checked properties.
It does not replace the source code or attempt to reproduce the entire program. His task is to fix the contract: which states are acceptable, which conditions must be met before the operation, and what must be true after it.
In a simplified way, it can be represented as:
Initial state
, ─
operation
│
▼
New conditionSJV describes the constraints on these states and the transitions between them.
Such a contract can already be negotiated regardless of the internal implementation. The customer does not need to know which algorithm the developer uses to achieve the result. It is important that the parties agree on which properties are considered mandatory.
In this sense, SJV becomes a technical contract between the one who creates the system and the one who must trust its behavior.
Verification is performed by the owner of the source code
With this scheme, the source code itself does not need to be transferred outside.
The developer performs verification in his environment. The verifying tool receives the implementation and the SJV contract, builds mathematical obligations and verifies them using a solver.
The simplified chain looks like this:
The source code
+
SJV
│
▼
The Verifier
│
▼
Mathematical obligations
│
▼
SMT solver
│
▼
SJPFor Sekura JS programs, the corresponding Sekura JS implementation is checked. A supported subset of SystemVerilog can be used for hardware descriptions.
The output is no longer the source code, but a separate SJP — Sekura Justified Proof file.
What is passed instead of the source code
SJP is designed to transfer the verification results.
In the current model, it links verification to specific inputs and contains information necessary to control the proof chain: mathematical obligations, hashes, contract information, dependencies, and signature.
You can transfer to the recipient:
SJV
+
SJP
+
public keyand leave the initial implementation inside the company.
Thus, the external participant does not receive the developer's promise in the form of the phrase "we checked everything", but a machine-verifiable artifact.
What can the recipient check?
After receiving the SJP, the other party can verify several different things.
First, you can check the integrity of the package. Hashes allow you to detect changes in related data or parts of the evidence chain.
Secondly, you can verify the signature. It allows you to set which key was used to sign a specific package. However, a valid signature by itself does not answer the question of who should be trusted with this key. This is a separate organizational decision of the parties.
Third, you can re-check the mathematical obligations contained in the SJP. In other words, the recipient does not have to simply trust the saved verification result.
It is the last point that is especially important. The proof becomes a portable object that can be rechecked separately from the environment where it was obtained.
Is it possible to double-check the proof with another solver?
Using a single mathematical solver creates a natural question: does the whole result depend on a specific tool?
Therefore, it is useful to keep mathematical obligations in a form that allows for repeated verification. In Sekura, the main process can use Z3, and compatible commitments can additionally be verified through cvc5.
The point here is not that two solvers automatically make any system error-free. They make it possible to reduce dependence on a single instance of the verification tool and detect discrepancies where independent re-verification is possible.
At the same time, it is necessary to maintain the exact boundaries of the statement. Re-checking the mathematical commitment confirms the result for this commitment. It does not automatically turn a formal model into a proof of all possible properties of a real system.
And how does the proof relate to closed source code?
This is the most important issue of the whole scheme.
If the recipient does not see the source code, they cannot independently read it and make sure that the implementation really meets their expectations. Therefore, the proof chain should be linked to a specific implementation version, not to its name.
For this purpose, cryptographic hashes and precise fixation of verification inputs are used.
The idea looks like this:
Implementation version
│
hash
│
├───────────────┐
▼ │
SJV │
│ │
▼ │
SJP verification
◄─
────────────┘If the implementation has changed, its hash will also change. The old SJP cannot be imperceptibly presented as evidence for the new version.
This does not reveal the contents of the source code, but it allows you to determine exactly which implementation the verification result belongs to.
Proof chains for large systems
A real system rarely consists of a single isolated module. One component calls another, which uses the third, and a dependency tree gradually emerges.
It is also not necessary to publish the source code of all components for compositional verification. A proven component can have its own SJP, and the next level of the system can refer to the already proven contracts of its dependencies.
It turns out a graph:
SJP of module A
│
├────────┐
─ ─
SJP of module B SJP of module C
, ─
SJP systemsThe parent proof records which specific dependency proofs it relies on.
As a result, it is possible to build a chain where each level is linked to the previous one in terms of content, and changing one of the components requires taking into account the change in the corresponding proof.
That formal verification without sources does not solve
It is important not to to attribute properties to such a scheme that it does not have.
SJP does not disclose the algorithm of the program and therefore does not replace the source code audit when an audit is necessary. Formal verification also does not prove properties that no one has formulated in the contract.
It does not automatically eliminate errors in the hardware model, compiler, verifier, mathematical solver, or assumptions made when setting the problem. Any evidence-based system has a trust boundary.
Therefore, the correct statement sounds something like this:
For the fixed version of the implementation, certain formal properties are checked under the specified assumptions, and the verification result is stored in an artifact that allows subsequent verification.
This is much more accurate than the phrase "the program is mathematically proven."
Where this approach is particularly useful
The separation of source code and proof is interesting primarily where two requirements exist simultaneously.: The implementation cannot be disclosed, but trusting the supplier alone is not enough.
For example, it can be hardware software, a closed library, an embedded system, a SystemVerilog block, a commercial algorithm, or a component supplied to several organizations.
The developer retains the intellectual property. The customer receives an accurate description of the verified properties and an artifact that is not reduced to a regular PDF report.
This changes the very subject of the exchange between the parties.
You can transmit not the source code, but a verifiable statement about a specific version of this code.
From "trust us" to a verifiable artifact
Closed source code usually creates a tough choice: either disclose the implementation to the auditor, or ask another party to trust the developer.
Formal evidentiary artifacts allow us to add a third option.
The implementation remains closed
↓
The properties are explicitly described
↓
The verification was completed formally
↓
The result is related to a specific implementation
↓
The evidence package can be transferred
↓
The recipient can check it.The source code remains with the owner.
The main idea here is not secrecy per se. She's in the role division: The implementation is responsible for how the system works; SJV determines what needs to be proved; SJP transfers the result of the performed verification.
Thus, formal verification can be used not only within the development process, but also as a way to transfer verifiable technical approvals between organizations without mandatory disclosure of the implementation.
Documentation
Technical description of Sekura JS.
Description of the SJV verification language.
Description of the supported subset of SystemVerilog.
The SJP specification and other verification materials are available in the Sekura JS documentation section.
Исходный код далеко не всегда можно передать заказчику, партнёру или аудитору. Он может содержать коммерческую тайну, собственные алгоритмы компании, лицензируемые компоненты или просто быть частью продукта, который поставляется только в двоичном виде.
При этом у другой стороны может быть вполне обоснованный вопрос: почему мы должны верить, что эта программа действительно обладает заявленными свойствами?
Обычный ответ — тесты, отчёты, сертификаты или аудит исходного кода. Но существует и другой вариант: формально описать требуемые свойства программы, математически проверить их и передать результат проверки отдельно от исходного кода.
Именно здесь появляется возможность разделить реализацию, требования к ней и доказательство.
Проверять нужно не «правильность вообще»
Фраза «программа формально проверена» сама по себе почти ничего не говорит. У любой проверки должны быть конкретные свойства.
Например, для управляющего модуля можно потребовать:
- счётчик никогда не выходит за допустимый диапазон;
- определённое состояние недостижимо;
- операция не изменяет защищённую область памяти;
- после выполнения функции выполняется заданное условие;
- переход из одного состояния в другое возможен только при определённых входных данных.
Формальная верификация отвечает не на вопрос:
Эта программа правильная?
А на более точный вопрос:
Выполняются ли заданные свойства для данной реализации в рамках принятой модели и указанных предположений?
Это принципиальное различие. Если некоторое свойство не было сформулировано, его отсутствие среди ошибок ещё не означает, что оно доказано.
Исходный код и контракт можно разделить
Представим компанию, которая разработала управляющий модуль для промышленного оборудования. Передавать его исходный код заказчику она не хочет, но заказчику необходимо убедиться, что модуль соблюдает несколько критических правил.
Можно разделить систему на три части:
Закрытая реализация
│
▼
Формальный контракт
│
▼
Проверяемое доказательствоРеализация остаётся у разработчика. Формальный контракт описывает свойства, которые должны выполняться. Результатом проверки становится отдельный доказательный артефакт.
В Sekura для этих двух последних частей используются SJV и SJP.
SJV описывает, что именно требуется доказать
SJV — язык описания проверяемых свойств.
Он не заменяет исходный код и не пытается воспроизвести всю программу. Его задача — зафиксировать контракт: какие состояния допустимы, какие условия должны выполняться до операции и что должно быть истинно после неё.
Упрощённо это можно представить так:
Исходное состояние
│
▼
операция
│
▼
Новое состояниеSJV описывает ограничения на эти состояния и переходы между ними.
Такой контракт уже можно обсуждать независимо от внутренней реализации. Заказчику необязательно знать, каким именно алгоритмом разработчик добивается результата. Важно, чтобы стороны договорились, какие свойства считаются обязательными.
В этом смысле SJV становится техническим договором между тем, кто создаёт систему, и тем, кто должен доверять её поведению.
Проверка выполняется у владельца исходного кода
Сам исходный код при такой схеме не требуется передавать наружу.
Разработчик выполняет верификацию в своей среде. Проверяющий инструмент получает реализацию и SJV-контракт, строит математические обязательства и проверяет их с помощью решателя.
Упрощённая цепочка выглядит так:
Исходный код
+
SJV
│
▼
Верификатор
│
▼
Математические обязательства
│
▼
SMT-решатель
│
▼
SJPДля программ Sekura JS проверяется соответствующая реализация Sekura JS. Для аппаратных описаний может использоваться поддерживаемое подмножество SystemVerilog.
На выходе получается уже не исходный код, а отдельный файл SJP — Sekura Justified Proof.
Что передаётся вместо исходного кода
SJP предназначен для переноса результатов проверки.
В текущей модели он связывает проверку с конкретными входными данными и содержит сведения, необходимые для контроля доказательной цепочки: математические обязательства, хеши, сведения о контрактах, зависимости и подпись.
Получателю можно передать:
SJV
+
SJP
+
публичный ключа исходную реализацию оставить внутри компании.
Таким образом, внешний участник получает не обещание разработчика в виде фразы «мы всё проверили», а машинно проверяемый артефакт.
Что может проверить получатель
Получив SJP, другая сторона может проверить несколько разных вещей.
Во-первых, можно проверить целостность пакета. Хеши позволяют обнаружить изменение связанных данных или частей доказательной цепочки.
Во-вторых, можно проверить подпись. Она позволяет установить, каким ключом был подписан конкретный пакет. При этом сама по себе действительная подпись ещё не отвечает на вопрос, кому следует доверять этот ключ. Это уже отдельное организационное решение сторон.
В-третьих, можно повторно проверить содержащиеся в SJP математические обязательства. То есть получатель не обязан просто доверять сохранённому результату проверки.
Именно последний пункт особенно важен. Доказательство становится переносимым объектом, который можно перепроверять отдельно от среды, где оно было получено.
Можно ли перепроверить доказательство другим решателем
Использование одного математического решателя создаёт естественный вопрос: не зависит ли весь результат от конкретного инструмента?
Поэтому математические обязательства полезно хранить в форме, допускающей повторную проверку. В Sekura основной процесс может использовать Z3, а совместимые обязательства могут дополнительно проверяться через cvc5.
Смысл здесь не в том, что два решателя автоматически делают любую систему безошибочной. Они позволяют уменьшить зависимость от единственного экземпляра проверяющего инструмента и обнаружить расхождения там, где независимая повторная проверка возможна.
При этом нужно сохранять точные границы утверждения. Повторная проверка математического обязательства подтверждает результат для этого обязательства. Она не превращает формальную модель автоматически в доказательство всех возможных свойств реальной системы.
А как доказательство связано с закрытым исходным кодом
Это самый важный вопрос всей схемы.
Если получатель не видит исходный код, он не может самостоятельно прочитать его и убедиться, что реализация действительно соответствует его ожиданиям. Поэтому доказательная цепочка должна быть связана с конкретной версией реализации, а не с её названием.
Для этого используются криптографические хеши и точная фиксация входов проверки.
Идея выглядит так:
Версия реализации
│
hash
│
├───────────────┐
▼ │
SJV │
│ │
▼ │
Верификация │
│ │
▼ │
SJP ◄─────────────┘Если реализация изменилась, её хеш тоже изменится. Старый SJP нельзя незаметно представить как доказательство для новой версии.
Это не раскрывает содержимое исходного кода, но позволяет точно определить, к какой реализации относится результат проверки.
Цепочки доказательств для больших систем
Реальная система редко состоит из одного изолированного модуля. Один компонент вызывает другой, тот использует третий, и постепенно возникает дерево зависимостей.
Публиковать исходный код всех компонентов для композиционной проверки также необязательно. Проверенный компонент может иметь собственный SJP, а следующий уровень системы — ссылаться на уже доказанные контракты его зависимостей.
Получается граф:
SJP модуля A
│
├────────┐
▼ ▼
SJP модуля B SJP модуля C
│
▼
SJP системыВ родительском доказательстве фиксируется, на какие конкретные доказательства зависимостей оно опирается.
В результате можно построить цепочку, где каждый уровень связан с предыдущим по содержимому, а изменение одного из компонентов требует учитывать изменение соответствующего доказательства.
Что формальная верификация без исходников не решает
Важно не приписывать такой схеме свойства, которых у неё нет.
SJP не раскрывает алгоритм программы и поэтому не заменяет аудит исходного кода, когда аудит необходим. Формальная проверка также не доказывает свойства, которые никто не сформулировал в контракте.
Она не устраняет автоматически ошибки в модели оборудования, компиляторе, верификаторе, математическом решателе или предположениях, сделанных при постановке задачи. У любой доказательной системы есть граница доверия.
Поэтому корректное утверждение звучит примерно так:
Для зафиксированной версии реализации проверены определённые формальные свойства при указанных предположениях, а результат проверки сохранён в артефакте, допускающем последующую проверку.
Это намного точнее, чем фраза «программа математически доказана».
Где такой подход особенно полезен
Разделение исходного кода и доказательства интересно прежде всего там, где одновременно существуют два требования: реализацию нельзя раскрывать, но одного доверия поставщику недостаточно.
Например, это может быть программное обеспечение оборудования, закрытая библиотека, встроенная система, блок SystemVerilog, коммерческий алгоритм или компонент, поставляемый нескольким организациям.
Разработчик сохраняет интеллектуальную собственность. Заказчик получает точное описание проверенных свойств и артефакт, который не сводится к обычному отчёту в PDF.
Это меняет сам предмет обмена между сторонами.
Передавать можно не исходный код, а проверяемое утверждение о конкретной версии этого кода.
От «поверьте нам» к проверяемому артефакту
Закрытый исходный код обычно создаёт жёсткий выбор: либо раскрыть реализацию аудитору, либо попросить другую сторону доверять разработчику.
Формальные доказательные артефакты позволяют добавить третий вариант.
Реализация остаётся закрытой
↓
Свойства описаны явно
↓
Проверка выполнена формально
↓
Результат связан с конкретной реализацией
↓
Доказательный пакет можно передать
↓
Получатель может его проверитьИсходный код при этом остаётся у владельца.
Главная идея здесь не в секретности как таковой. Она в разделении ролей: реализация отвечает за то, как работает система; SJV определяет, что требуется доказать; SJP переносит результат выполненной проверки.
Так формальная верификация может использоваться не только внутри процесса разработки, но и как способ передавать проверяемые технические утверждения между организациями без обязательного раскрытия реализации.
Документация
Техническое описание Sekura JS.
Описание языка верификации SJV.
Описание поддерживаемого подмножества SystemVerilog.
Спецификация SJP и остальные материалы по верификации доступны в разделе документации Sekura JS.
Share
