The post has been translated automatically. Original language: Russian
Formal verification allows you to confirm a specific property of a program or a hardware module. However, the verification result itself may lose practical value over time if it is impossible to determine which version of the system it belonged to, which source data was used, and what exactly was confirmed.
As the project develops, new versions of the source code appear, requirements change, bugs are fixed, and development tools are updated. In such a situation, it is important to keep not only individual audit reports, but also the entire relationship between the requirement, implementation and the result.
To do this, we are developing Sekura Noda Assurance, a separate Noda layer for maintaining an evidence—based history of an engineering project.
Why reports alone are not enough
Let's imagine that some property of the system has been successfully tested. The developer saved the report and continued working.
After a few months, the source code changed. There is a new version of the compiler, the hardware module has changed, or the requirements have been clarified.
The old report itself has not disappeared anywhere. But now it is necessary to understand whether it relates to the current state of the project.
If the relationship between the verification result and a specific implementation version has not been preserved in advance, it becomes difficult to answer this question. You have to manually study the source code history, old files, reports, and developer records.
This is still possible in a small project. In a system with a lot of requirements and checks, this approach quickly stops working.
From requirement to proof
At Sekura Noda Assurance, we try to maintain the entire chain that led to the verification result.
It starts with a requirement. The requirement defines the property that the system must provide.
Then the verification description and the specific implementation version to which this requirement applies are recorded. After the verification is completed, its initial data, the tool used, the result, and supporting materials are saved.
The result is a related sequence.:
requirement → verification description → implementation version → completed verification → evidence → fixed project status
This structure allows you to later restore not only the result, but also its origin.
The proof must relate to a specific version.
One of the basic rules is that the result should not be separated from the implementation version.
If the verification was performed for a certain state of the source code, the received proof belongs to it.
After changing the code, the old result does not become incorrect. It still confirms the property of the previous version.
But it is no longer possible to use it as proof for the new version without additional verification.
Therefore, Sekura Noda Assurance allows you to compare evidence materials with the current state of the project and determine which of them continue to correspond to the used implementation, and which require updating.
How to see untested requirements
In an engineering project, it is rare for all requirements to be confirmed at the same time.
Some properties have already been verified, tests or formal models are still being prepared for others, and others have just appeared in the new version of the requirements.
Sekura Noda Assurance allows you to see such gaps directly.
Instead of the general statement "the project has been verified", you can look at each requirement and determine if there is the necessary confirmation for it.
If there is no proof yet, it is fixed as an open gap. This result is more useful than trying to hide unfinished work, as it shows the real state of the project.
Formal verification is not the only way to confirm
Different verification methods are suitable for different requirements.
Some properties can be confirmed by formal methods. Others are more reasonable to check with tests. In some cases, reproducibility of the assembly or an engineering review of the result by a specialist is required.
Sekura Noda Assurance allows you to account for different types of confirmations in one system.
However, they are not automatically considered equivalent. For each requirement, you can determine which type of verification is required.
For example, a successful test may be sufficient for one property. The other requires a formal proof. For the third one, several independent confirmations may be required at the same time.
Why record the project status?
At a certain point in development, it is necessary to be able to say: here is the version of the system and here is the evidence base that existed specifically for it.
To do this, you can create an immutable project control state in Sekura Noda Assurance.
It records requirements, implementation versions, audit results, and related evidentiary materials.
When a new version of the system appears later, the states can be compared with each other. This allows you to see which requirements have changed, which implementations have been updated, and which results now need to be retrieved.
This is how the history of evidence develops along with the history of the project itself.
What happens after the component is changed
Changing one low-level component may affect several requirements at once.
For example, changing the compiler can affect the machine code of several programs. Changing the processor module may affect properties that were previously checked for the previous hardware version.
If the connections between these objects are preserved in advance, the consequences of the change can be determined much more accurately.
Sekura Noda Assurance stores the relationship between requirements, implementation versions, and validation results. Therefore, after the change, you can see which confirmations have potentially become outdated and require re-work.
This is especially important for large systems where the developer can no longer keep all the dependencies in memory.
Why is evidence being recorded?
The verification result first appears as working material. It must be linked to the correct requirement, check the source data and make sure that the necessary files are attached.
After confirmation, such a result can be fixed as an unchangeable part of the evidence base.
If the system changes later, the old result is not overwritten. A new confirmation is created for the new version.
This preserves the real history of the system's development. You can see what was proven for the previous version and what changed after the next release.
Why save checksums?
For the evidence base, not only the file name is important, but also its exact contents.
Therefore, the initial data and results can be associated with checksums. If the contents of the file have changed by at least one byte, its checksum also changes.
This allows you to determine exactly which file was involved in the verification.
This is especially important for source code, machine objects, formal descriptions, test reports, and evidence packages.
Thus, the result is associated not just with a file with a specific name, but with its specific contents.
Relation to requirements for reliable systems
Such an evidence-based story is necessary in areas where increased reliability of software and hardware is required.
In such projects, it is not enough to show only the final code or device. It is necessary to understand the origin of the requirements, the history of changes, verification methods, and specific results confirming the claimed properties.
That is why we consider Sekura Noda Assurance as the basis for further work with systems that have serious safety and reliability requirements.
At the same time, the Assurance system itself is not a certification body and does not issue an opinion on compliance with industry standards.
It solves a more fundamental problem — it helps to conduct development so that an evidence-based story is created simultaneously with the product.
Do not restore history retroactively
One of the most difficult situations arises when the evidence base begins to be collected only before external verification.
By this time, the project may have been in existence for several years. Some of the solutions have been forgotten, old versions of the tools are unavailable, some source data has been changed, and the test results are in different places.
We have to restore the development history retroactively.
We want to avoid this the approach.
Sekura Noda Assurance allows you to maintain the link between requirements, implementation, and checks directly during development.
Then, a year later, you don't need to remember why a certain property was considered confirmed. You can open the relevant requirement and see the entire evidence history related to it.
What is Sekura Noda Assurance for in the end?
The main task of Sekura Noda Assurance is not file storage.
Files can be saved in a regular repository or in a source code management system. The problem begins when it is necessary to understand the relationship between them.
What requirement does this report confirm? Which version of the source code does it belong to? How was the verification performed? Has anything changed since then? Do I need to repeat the check for the current version?
Sekura Noda Assurance is created so that such questions can be answered accurately.
For projects where the properties of the system must not only be declared, but also confirmed, such traceability becomes an important part of the development itself.
Формальная проверка позволяет подтвердить конкретное свойство программы или аппаратного модуля. Но сам результат проверки со временем может потерять практическую ценность, если невозможно установить, к какой версии системы он относился, какие исходные данные использовались и что именно было подтверждено.
По мере развития проекта появляются новые версии исходного кода, меняются требования, исправляются ошибки и обновляются средства разработки. В такой ситуации важно сохранять не только отдельные отчёты о проверках, но и всю связь между требованием, реализацией и полученным результатом.
Для этого мы развиваем Sekura Noda Assurance — отдельный слой Noda для ведения доказательной истории инженерного проекта.
Почему одних отчётов недостаточно
Представим, что некоторое свойство системы было успешно проверено. Разработчик сохранил отчёт и продолжил работу.
Через несколько месяцев исходный код изменился. Появилась новая версия компилятора, изменился аппаратный модуль или были уточнены требования.
Сам старый отчёт никуда не исчез. Но теперь необходимо понять, относится ли он к текущему состоянию проекта.
Если связь между результатом проверки и конкретной версией реализации не была сохранена заранее, ответить на этот вопрос становится трудно. Приходится вручную изучать историю исходного кода, старые файлы, отчёты и записи разработчиков.
В небольшом проекте это ещё возможно. В системе с большим количеством требований и проверок такой подход быстро перестаёт работать.
От требования до доказательства
В Sekura Noda Assurance мы стараемся сохранять всю цепочку, которая привела к результату проверки.
Она начинается с требования. Требование определяет свойство, которое система должна обеспечивать.
Затем фиксируется описание проверки и конкретная версия реализации, к которой это требование относится. После выполнения проверки сохраняются её исходные данные, использованный инструмент, результат и подтверждающие материалы.
В итоге получается связанная последовательность:
требование → описание проверки → версия реализации → выполненная проверка → доказательный материал → зафиксированное состояние проекта
Такая структура позволяет позже восстановить не только результат, но и его происхождение.
Доказательство должно относиться к конкретной версии
Одно из основных правил заключается в том, что результат нельзя отделять от версии реализации.
Если проверка была выполнена для определённого состояния исходного кода, именно к нему и относится полученное доказательство.
После изменения кода старый результат не становится неправильным. Он по-прежнему подтверждает свойство прежней версии.
Но использовать его как доказательство для новой версии без дополнительной проверки уже нельзя.
Поэтому Sekura Noda Assurance позволяет сравнивать доказательные материалы с текущим состоянием проекта и определять, какие из них продолжают соответствовать используемой реализации, а какие требуют обновления.
Как увидеть непроверенные требования
В инженерном проекте редко бывает ситуация, когда все требования подтверждены одновременно.
Одни свойства уже проверены, для других ещё готовятся тесты или формальные модели, а третьи только появились в новой версии требований.
Sekura Noda Assurance позволяет видеть такие пробелы напрямую.
Вместо общего утверждения «проект проверен» можно посмотреть на каждое требование и определить, существует ли для него необходимое подтверждение.
Если доказательства пока нет, это фиксируется как открытый пробел. Такой результат полезнее, чем попытка скрыть незавершённую работу, поскольку показывает реальное состояние проекта.
Формальная проверка — не единственный способ подтверждения
Для разных требований подходят разные методы проверки.
Некоторые свойства можно подтвердить формальными методами. Другие разумнее проверять испытаниями. В отдельных случаях требуется воспроизводимость сборки или инженерное рассмотрение результата специалистом.
Sekura Noda Assurance позволяет учитывать разные виды подтверждений в одной системе.
При этом они не считаются равнозначными автоматически. Для каждого требования можно определить, какой вид проверки необходим.
Например, для одного свойства может быть достаточно успешного испытания. Для другого потребуется формальное доказательство. Для третьего могут одновременно потребоваться несколько независимых подтверждений.
Зачем фиксировать состояние проекта
В определённый момент разработки необходимо иметь возможность сказать: вот версия системы и вот доказательная база, которая существовала именно для неё.
Для этого в Sekura Noda Assurance можно создавать неизменяемое контрольное состояние проекта.
В нём фиксируются требования, версии реализации, результаты проверок и связанные доказательные материалы.
Когда позже появляется новая версия системы, состояния можно сравнить между собой. Это позволяет увидеть, какие требования изменились, какие реализации были обновлены и какие результаты теперь необходимо получить заново.
Так история доказательств развивается вместе с историей самого проекта.
Что происходит после изменения компонента
Изменение одного низкоуровневого компонента может затронуть сразу несколько требований.
Например, изменение компилятора способно повлиять на машинный код нескольких программ. Изменение процессорного модуля может затронуть свойства, которые ранее были проверены для предыдущей версии аппаратуры.
Если связи между этими объектами заранее сохранены, последствия изменения можно определить значительно точнее.
Sekura Noda Assurance хранит отношения между требованиями, версиями реализации и результатами проверки. Поэтому после изменения можно увидеть, какие подтверждения потенциально стали устаревшими и требуют повторной работы.
Это особенно важно для больших систем, где разработчик уже не может удерживать все зависимости в памяти.
Почему доказательный материал фиксируется
Результат проверки сначала появляется как рабочий материал. Его необходимо связать с правильным требованием, проверить исходные данные и убедиться, что приложены необходимые файлы.
После подтверждения такой результат можно зафиксировать как неизменяемую часть доказательной базы.
Если позже система изменяется, старый результат не переписывается. Для новой версии создаётся новое подтверждение.
Благодаря этому сохраняется реальная история развития системы. Можно увидеть, что было доказано для предыдущей версии и что изменилось после следующего выпуска.
Зачем сохранять контрольные суммы
Для доказательной базы важно не только имя файла, но и его точное содержимое.
Поэтому исходные данные и результаты могут связываться с контрольными суммами. Если содержимое файла изменилось хотя бы на один байт, меняется и его контрольная сумма.
Это позволяет точно определить, какой именно файл участвовал в проверке.
Особенно это важно для исходного кода, машинных объектов, формальных описаний, отчётов испытаний и доказательных пакетов.
Таким образом, результат связывается не просто с файлом с определённым названием, а с его конкретным содержимым.
Связь с требованиями к надёжным системам
Подобная доказательная история необходима в областях, где требуется повышенная надёжность программного и аппаратного обеспечения.
В таких проектах недостаточно показать только конечный код или устройство. Необходимо понимать происхождение требований, историю изменений, способы проверки и конкретные результаты, подтверждающие заявленные свойства.
Именно поэтому мы рассматриваем Sekura Noda Assurance как основу для дальнейшей работы с системами, к которым предъявляются серьёзные требования по безопасности и надёжности.
При этом сама система Assurance не является органом сертификации и не выдаёт заключение о соответствии отраслевым стандартам.
Она решает более фундаментальную задачу — помогает вести разработку так, чтобы доказательная история создавалась одновременно с продуктом.
Не восстанавливать историю задним числом
Одна из самых сложных ситуаций возникает, когда доказательную базу начинают собирать только перед внешней проверкой.
К этому времени проект может существовать уже несколько лет. Часть решений забыта, старые версии инструментов недоступны, некоторые исходные данные изменены, а результаты испытаний находятся в разных местах.
Приходится восстанавливать историю разработки задним числом.
Мы хотим избежать такого подхода.
Sekura Noda Assurance позволяет сохранять связь между требованиями, реализацией и проверками непосредственно во время разработки.
Тогда через год не нужно вспоминать, почему некоторое свойство считалось подтверждённым. Можно открыть соответствующее требование и увидеть всю связанную с ним доказательную историю.
Для чего в итоге нужен Sekura Noda Assurance
Главная задача Sekura Noda Assurance — не хранение файлов.
Файлы можно сохранить в обычном хранилище или в системе управления исходным кодом. Проблема начинается тогда, когда требуется понять взаимосвязь между ними.
Какое требование подтверждает этот отчёт? К какой версии исходного кода он относится? Каким способом была выполнена проверка? Изменилось ли что-нибудь после неё? Нужно ли повторять проверку для текущей версии?
Sekura Noda Assurance создаётся для того, чтобы на такие вопросы можно было получить точный ответ.
Для проектов, где свойства системы должны быть не только заявлены, но и подтверждены, такая прослеживаемость становится важной частью самой разработки.
Share
