The post has been translated automatically. Original language: Russian
Most programs and digital devices are tested using tests. The developer sets the input data, runs the program or hardware model, and compares the result with the expected result.
This approach is necessary, but it has an obvious limitation: the test shows that the system worked correctly in specific proven cases. It does not prove that the error does not exist in some other combination of input data and states.
Formal verification is trying to answer another question.: is it possible to prove mathematically that a given property of the system holds for all states that are included in the model being tested?
That is why formal methods are particularly interesting for processors, operating systems, industrial software, and other systems where a rare error can have a significantly higher cost than a typical software failure.
Testing and proof answer different questions
Let's imagine a simple function that accepts two 32-bit numbers.
You can write a thousand tests, a million tests, or randomly test even more options. If all of them are successful, confidence in the program increases.
But the number of possible pairs of 32-bit values is huge.:
2^32 × 2^32 = 2^64It is almost impossible to test each option with a regular launch.
The formal approach works differently. Instead of listing specific values, the input data is set symbolically, after which the checker examines all possible options simultaneously and tries to prove a given statement.
For example:
for any valid a and b
, the result of the function follows the specified ruleIf a proof is obtained, it applies not to one thousand selected examples, but to the entire state space described in the model.
Formal verification begins with the property
The most important part of verification is not the means of proof, but the precise formulation of what exactly needs to be proved.
For example, you can set properties for a queue:
if the queue is empty, reading does not return the old item.
if the queue is full, the new entry does not corrupt the existing data.
the order of the elements is preservedThe properties may be different for memory management.:
The processor does not access a page
that it does not own.
Two tasks cannot simultaneously gain
exclusive ownership of one page.For an arithmetic block, you can check whether the result matches the mathematical definition of the operation.
Formal verification therefore does not mean the abstract "prove the program correct". First, it is necessary to determine the specific properties regarding which the system is considered correct.
What happens during the check
The simplified process looks like this:
Description of the system
+
formal properties
↓
mathematical model
↓
means of proof
↓
property proved
or
counterexample foundA counterexample is especially useful. If the property is violated, the checker can show a sequence of states leading to an error.
It looks like an automatically found test, but such a test does not appear by chance. It is a concrete proof that the stated property of the system is incorrect.
The developer does not just receive the message "verification failed", but the path to the state in which the violation occurs.
Why is this different from static analysis?
Static analyzers also examine the program without running it normally. They can find potential errors, memory malfunctions, unreachable code, or suspicious designs.
However, formal verification poses a more rigorous task.
If the static analyzer says:
there may be a mistake herethat means of formal verification is trying to determine:
can such an error actually occur
under the conditions of a given model?or prove that it is impossible.
At the same time, the boundary between approaches is not always absolute: modern development tools can combine several methods.
How is the program formally checked?
For a regular program, you can describe the state before the function is executed and the state after it.
For example, the function should increment the counter:
before:
counter = N
after:
counter = N + 1But the actual program almost always requires more complex conditions.
You can specify that:
a pointer is acceptable
the buffer size does not exceed the limit
The rest of the data should not change.
the result is within the acceptable rangeAfter that, it is checked that each possible branch of the program retains these properties.
This is how you can prove individual functions, modules, and small algorithms.
Why is it harder to check large programs?
The problem of formal verification is the growth of the state space.
Each variable, branch, loop, execution flow, and part of the memory increases the number of possible system states.
For a small block, there may be relatively few of them. For a complete modern operating system, the number of combinations becomes huge.
Therefore, large systems rarely try to prove themselves as one monolith.
A different approach is used: the system is divided into components, each with its own contract, and then the properties of the individual parts and the rules for their interaction are proved.
That is why architectural simplicity becomes important not only for implementation, but also for the possibility of verification.
What can be checked in the operating system
The operating system is located between the program and the hardware, so its properties are especially important.
For example, you can check the insulation:
process A cannot read the memory of process B
without an explicitly allowed mechanism.You can check resource management:
the same memory page
cannot belong
to two independent owners at the same timeYou can formalize system calls, context switching, queue operation, and privilege change rules.
Systems where the number of basic states and transitions is intentionally limited are particularly well verifiable.
If the architecture of an operating system contains dozens of hidden mechanisms and a large number of implicit states, the proof becomes much more difficult.
Is it possible to formally check the processor
Yes. A digital circuit is also a system of states.
The processor registers form the current state, the input signals set the effects, and the clock transition determines the next state.
You can, for example, check:
ADD always performs the required addition
an invalid command does not change
the architectural state.
switching to a new address really
cancels out the younger teams.
writing to memory takes place
only under the allowed condition.For a pipelined processor, it is especially important to prove the correspondence between a complex internal implementation and a simpler architectural model.
That is, it must be shown that, regardless of the internal stages, the processor behaves as required by the description of its instruction set.
Checking the processor does not mean checking the transistors.
Formal verification always has a level of abstraction.
If we check the processor description in the language of digital circuits, then we prove the properties of this particular model.
There are other stages between it and the physical crystal:
Circuit description
↓
synthesis
↓
placement
↓
tracing
↓
physical crystalEach transition adds its own assumptions and tools.
Therefore, it is more correct to say not "the processor is fully proven", but to specify exactly which model has been tested and which properties have been proven for it.
This rule applies to all formal verification.
The proof always has boundaries
Any formal proof is constructed relative to some model.
If the model assumes:
The memory works without physical errorsthat proof doesn't say anything about the cell being damaged due to a hardware defect.
If the processor model does not include a specific The I/O device, processor proof is not automatically distributed to this device.
If the compiler is outside of the test loop, it is assumed that it correctly converts the source program into machine code.
Therefore, one of the main issues of formal verification is not only:
What has been proven?but also:
What do you still have to trust?This remaining set of untested components is often referred to as the trusted backbone of the system.
The smaller the trusted base, the better
Let's imagine a chain:
the source code
↓
compiler
↓
machine program
↓
operating system
↓
processor
↓
hardware devicesIf only the original function has been formally verified, but the compiler or operating system can change its behavior, the final proof is of limited force.
Therefore, the long—term goal of formal methods is not necessarily to prove absolutely everything, but to reduce the number of components that have to be trusted without independent verification.
You can check different levels and link the results together.
This is where the idea of a testable computing stack comes in.
The program and the processor should be talking about the same thing.
There is another important problem: different levels of the system may have different representations of a single operation.
The program considers that a single operation is being performed, the compiler converts it into several machine instructions, and the processor executes them through many internal states.
If the properties of each level are formulated independently, gaps may remain between the proofs.
A stronger approach is to create a common formal semantics.:
what does the operation mean in the language?
how is it converted to machine code?
what should a machine command do?
how is this implemented in the hardware?Then the proof of one level can be linked to the proof of the next.
This is much more complicated, but it is this approach that allows us to talk no longer about a separate proven module, but about a verifiable chain of calculations.
Why simple architecture helps
Formal verification is not free.
The more hidden states, special cases, and exceptions a system contains, the more complex its model and proof are.
Therefore, solutions that seem to be architecture limitations sometimes give an advantage in the level of verifiability.
For example:
a small set of machine commands
Simple memory rules
explicit ownership of resources
limited number of device types
short and unambiguous state transitionsall these properties reduce the space that needs to be analyzed.
The processor may be less versatile at the level of individual mechanisms, but it is much more understandable as a whole system.
Formal verification does not cancel the tests.
Evidence and testing should not be contrasted.
The tests are good at finding practical implementation errors, problems interacting with real equipment, time violations, and many situations that are not included in the formal model.
Formal verification, in turn, examines all possible states well within an explicitly defined model.
Therefore, the most reliable approach combines several methods:
formal verification of properties
tests
simulation
checking on real hardwareEach method answers its own part of the question about the correctness of the system.
From "it" to "you can explain why it works"
In conventional development, a system that has passed a set of tests is often considered a sufficient result.
This may not be enough for mission-critical calculations.
Formal verification offers another level of requirement: the developer must not only show a working example, but also formulate precisely which properties of the system are mandatory and why they cannot be violated within a given model.
This changes the very approach to architecture.
The system has to be designed so that its states and transitions can be described accurately enough. Therefore, formal verification does not become the last stage of checking the finished product, but one of the factors affecting the design of programs, the operating system and the processor from the very beginning.
The main idea here is simple: testing shows that the error did not appear in the verified cases. Formal verification attempts to prove that a certain class of errors is impossible in the entire state space of a given model.
And the closer the software comes to managing industrial equipment, infrastructure, and other mission-critical systems, the more valuable this opportunity becomes.
Большинство программ и цифровых устройств проверяют с помощью тестов. Разработчик задаёт входные данные, запускает программу или аппаратную модель и сравнивает полученный результат с ожидаемым.
Такой подход необходим, но у него есть очевидное ограничение: тест показывает, что система правильно сработала в конкретных проверенных случаях. Он не доказывает, что ошибка не существует в каком-то другом сочетании входных данных и состояний.
Формальная верификация пытается ответить на другой вопрос: можно ли математически доказать, что заданное свойство системы выполняется для всех состояний, которые входят в проверяемую модель?
Именно поэтому формальные методы особенно интересны для процессоров, операционных систем, промышленного программного обеспечения и других систем, где редкая ошибка может иметь значительно большую стоимость, чем обычный программный сбой.
Тестирование и доказательство отвечают на разные вопросы
Представим простую функцию, принимающую два 32-битных числа.
Можно написать тысячу тестов, миллион тестов или случайным образом проверить ещё больше вариантов. Если все они проходят успешно, уверенность в программе растёт.
Но количество возможных пар 32-битных значений огромно:
2^32 × 2^32 = 2^64Проверить каждый вариант обычным запуском практически невозможно.
Формальный подход устроен иначе. Вместо перечисления конкретных значений входные данные задаются символически, после чего средство проверки исследует все допустимые варианты одновременно и пытается доказать заданное утверждение.
Например:
для любых допустимых a и b
результат функции соответствует заданному правилуЕсли доказательство получено, оно относится не к одной тысяче выбранных примеров, а ко всему пространству состояний, описанному в модели.
Формальная верификация начинается со свойства
Самая важная часть проверки — не средство доказательства, а точная формулировка того, что именно требуется доказать.
Например, для очереди можно задать свойства:
если очередь пуста, чтение не возвращает старый элемент
если очередь заполнена, новая запись не повреждает существующие данные
порядок элементов сохраняетсяДля управления памятью свойства могут быть другими:
процессор не получает доступ к странице,
которой он не владеет
две задачи не могут одновременно получить
исключительное владение одной страницейДля арифметического блока можно проверять соответствие результата математическому определению операции.
Формальная верификация поэтому не означает абстрактное «доказать программу правильной». Сначала необходимо определить конкретные свойства, относительно которых система считается правильной.
Что происходит во время проверки
Упрощённо процесс выглядит так:
описание системы
+
формальные свойства
↓
математическая модель
↓
средство доказательства
↓
свойство доказано
или
найден контрпримерКонтрпример особенно полезен. Если свойство нарушается, средство проверки может показать последовательность состояний, приводящую к ошибке.
Это похоже на автоматически найденный тест, но такой тест появляется не случайно. Он является конкретным доказательством того, что заявленное свойство системы неверно.
Разработчик получает не просто сообщение «проверка не прошла», а путь к состоянию, в котором возникает нарушение.
Почему это отличается от статического анализа
Статические анализаторы также изучают программу без обычного запуска. Они могут находить потенциальные ошибки, неправильную работу с памятью, недостижимый код или подозрительные конструкции.
Однако формальная верификация ставит более строгую задачу.
Если статический анализатор говорит:
здесь возможна ошибкато средство формальной проверки пытается определить:
может ли такая ошибка реально возникнуть
при условиях заданной моделиили доказать, что она невозможна.
При этом граница между подходами не всегда абсолютна: современные средства разработки могут сочетать несколько методов.
Как формально проверяют программу
Для обычной программы можно описать состояние до выполнения функции и состояние после неё.
Например, функция должна увеличить счётчик:
до:
counter = N
после:
counter = N + 1Но реальная программа почти всегда требует более сложных условий.
Можно указать, что:
указатель допустим
размер буфера не превышает границу
остальные данные не должны измениться
результат находится в допустимом диапазонеПосле этого проверяется, что каждая возможная ветвь программы сохраняет эти свойства.
Так можно доказывать отдельные функции, модули и небольшие алгоритмы.
Почему большие программы проверять сложнее
Проблема формальной верификации заключается в росте пространства состояний.
Каждая переменная, ветвление, цикл, поток выполнения и часть памяти увеличивают количество возможных состояний системы.
Для небольшого блока их может быть относительно немного. Для полной современной операционной системы число комбинаций становится огромным.
Поэтому большие системы редко пытаются доказать как один монолит.
Используется другой подход: систему разделяют на компоненты, для каждого задают собственный контракт, а затем доказывают свойства отдельных частей и правила их взаимодействия.
Именно поэтому архитектурная простота становится важной не только для реализации, но и для возможности проверки.
Что можно проверять в операционной системе
Операционная система находится между программой и аппаратурой, поэтому её свойства особенно важны.
Например, можно проверять изоляцию:
процесс A не может читать память процесса B
без явно разрешённого механизмаМожно проверять управление ресурсами:
одна и та же страница памяти
не может одновременно принадлежать
двум независимым владельцамМожно формализовать системные вызовы, переключение контекста, работу очередей и правила изменения привилегий.
Особенно хорошо формальной проверке поддаются системы, где число основных состояний и переходов намеренно ограничено.
Если архитектура операционной системы содержит десятки скрытых механизмов и большое количество неявных состояний, доказательство становится значительно сложнее.
Можно ли формально проверить процессор
Да. Цифровая схема тоже является системой состояний.
Регистры процессора образуют текущее состояние, входные сигналы задают воздействия, а тактовый переход определяет следующее состояние.
Можно, например, проверить:
ADD всегда выполняет требуемое сложение
недопустимая команда не изменяет
архитектурное состояние
переход на новый адрес действительно
отменяет более молодые команды
запись в память происходит
только при разрешённом условииДля конвейерного процессора особенно важно доказать соответствие между сложной внутренней реализацией и более простой архитектурной моделью.
То есть необходимо показать, что независимо от внутренних стадий процессор ведёт себя так, как требует описание его набора команд.
Проверять процессор — не значит проверять транзисторы
У формальной верификации всегда есть уровень абстракции.
Если мы проверяем описание процессора на языке цифровых схем, то доказываем свойства именно этой модели.
Между ней и физическим кристаллом остаются другие этапы:
описание схемы
↓
синтез
↓
размещение
↓
трассировка
↓
физический кристаллКаждый переход добавляет собственные предположения и инструменты.
Поэтому корректнее говорить не «процессор полностью доказан», а точно указывать, какая модель проверена и какие свойства для неё доказаны.
Это правило относится ко всей формальной верификации.
Доказательство всегда имеет границы
Любое формальное доказательство строится относительно некоторой модели.
Если в модели предполагается:
память работает без физических ошибокто доказательство не говорит ничего о повреждении ячейки из-за аппаратного дефекта.
Если модель процессора не включает конкретное устройство ввода-вывода, доказательство процессора не распространяется автоматически на это устройство.
Если компилятор находится вне проверяемого контура, остаётся предположение, что он правильно преобразует исходную программу в машинный код.
Поэтому один из главных вопросов формальной верификации звучит не только:
что доказано?но и:
чему всё ещё приходится доверять?Этот оставшийся набор непроверенных компонентов часто называют доверенной основой системы.
Чем меньше доверенная основа, тем лучше
Представим цепочку:
исходный код
↓
компилятор
↓
машинная программа
↓
операционная система
↓
процессор
↓
аппаратные устройстваЕсли формально проверена только исходная функция, но компилятор или операционная система могут изменить её поведение, итоговое доказательство имеет ограниченную силу.
Поэтому долгосрочная цель формальных методов — не обязательно доказать абсолютно всё, а уменьшить количество компонентов, которым приходится доверять без независимой проверки.
Можно проверять разные уровни и связывать результаты между собой.
Именно здесь появляется идея проверяемого вычислительного стека.
Программа и процессор должны говорить об одном
Есть ещё одна важная проблема: разные уровни системы могут иметь разные представления одной операции.
Программа считает, что выполняется одна операция, компилятор преобразует её в несколько машинных команд, процессор исполняет их через множество внутренних состояний.
Если свойства каждого уровня сформулированы независимо, между доказательствами могут оставаться разрывы.
Более сильный подход состоит в создании общей формальной семантики:
что означает операция в языке
как она преобразуется в машинный код
что должна делать машинная команда
как это реализовано в аппаратуреТогда доказательство одного уровня можно связывать с доказательством следующего.
Это значительно сложнее, но именно такой подход позволяет говорить уже не об отдельном проверенном модуле, а о проверяемой цепочке вычислений.
Почему простая архитектура помогает
Формальная верификация не является бесплатной.
Чем больше скрытых состояний, специальных случаев и исключений содержит система, тем сложнее её модель и доказательство.
Поэтому решения, которые кажутся ограничениями архитектуры, иногда дают преимущество на уровне проверяемости.
Например:
небольшой набор машинных команд
простые правила памяти
явное владение ресурсами
ограниченное число типов устройств
короткие и однозначные переходы состоянийвсе эти свойства уменьшают пространство, которое необходимо анализировать.
Процессор может быть менее универсальным на уровне отдельных механизмов, но значительно более понятным как целая система.
Формальная верификация не отменяет тесты
Доказательства и тестирование не следует противопоставлять.
Тесты хорошо находят практические ошибки реализации, проблемы взаимодействия с реальным оборудованием, нарушения временных характеристик и множество ситуаций, которые не вошли в формальную модель.
Формальная проверка, в свою очередь, хорошо исследует все допустимые состояния внутри явно заданной модели.
Поэтому наиболее надёжный подход сочетает несколько методов:
формальная проверка свойств
тесты
моделирование
проверка на реальном оборудованииКаждый метод отвечает на свою часть вопроса о корректности системы.
От «работает» к «можно объяснить, почему работает»
В обычной разработке достаточным результатом часто считается система, прошедшая набор тестов.
Для критически важных вычислений этого может быть недостаточно.
Формальная верификация предлагает другой уровень требования: разработчик должен не только показать работающий пример, но и точно сформулировать, какие свойства системы являются обязательными и почему они не могут быть нарушены в пределах заданной модели.
Это меняет сам подход к архитектуре.
Систему приходится проектировать так, чтобы её состояния и переходы можно было описать достаточно точно. Поэтому формальная верификация становится не последним этапом проверки готового продукта, а одним из факторов, влияющих на устройство программ, операционной системы и процессора с самого начала.
Главная идея здесь проста: тестирование показывает, что ошибка не проявилась в проверенных случаях. Формальная верификация пытается доказать, что определённый класс ошибок невозможен во всём пространстве состояний заданной модели.
И чем ближе программное обеспечение подходит к управлению промышленным оборудованием, инфраструктурой и другими критически важными системами, тем ценнее становится такая возможность.
Share
