The post has been translated automatically. Original language: Russian
Formally, it is much easier to verify a single function than an entire computing system. Even if the source program is proven to perform the desired property, the compiler, machine code, operating system, and processor remain between it and the actual result.
Each such level can change the behavior of the system or add its own error. Therefore, for Memora8, we are exploring a broader task.: is it possible to link the verification of the program, machine code, operating system and processor in one sequential chain?
For this purpose, the SJV system of formal specifications, the Memora8 processor and the Reganta operating system are being developed next to the Sekura JS language.
The goal is not to put a "proven" stamp on the entire system one day. It is much more important to know exactly which properties have been tested, about which implementation they have been proven, and where the boundaries of trust remain.
Why is the evidence of individual components insufficient
Let's imagine that we have proved the correctness of some function at the source language level.:
source program
↓
The property is provedBut then the compiler converts this program.:
source program
↓
compiler
↓
machine codeIf the compiler makes a mistake, the proven property of the source program no longer guarantees the correctness of the executable code.
Next, the machine code is executed by the processor:
machine code
↓
processorIf the processor implements one of the commands differently than the language model suggests, another gap occurs.
There is also an operating system between them that manages memory, device access, and system actions.
As a result, the real chain looks much longer.:
source program
↓
compiler
↓
machine program
↓
operating system
↓
processor
↓
hardware devicesTherefore, checking only the first link leaves too many assumptions about all subsequent links.
SJV's idea: to separate the program from its properties
In the Sekura system, the program and its formal specification exist separately.
For example:
motor.sjs
motor.sjvThe Sekura JS file contains an implementation, and SJV describes the properties that this implementation must match.
This is an important division. We are not trying to consider the program code itself as its own proof. The specification is set separately and can, for example, describe acceptable device states.:
Mode = operation
speed < 100
error = 0or another valid condition:
Mode = crash
speed = 0
engine disabledThus, SJV does not describe a sequence of commands, but rather the boundaries of acceptable behavior.
The status is checked before and after the action
For a single function, you can set conditions for the state before and after its execution.
For example, a speed change operation may have the following meaning:
Before execution:
new speed < 100
after execution:
speed = new valueIn SJV, the values after execution are designated separately from the initial state. Due to this, the specification describes the transition:
state before
↓
operation
↓
state afterThe verifying system must establish that the actual implementation of the function does indeed lead only to such states as are permitted by the specification.
This is already different from the usual test. We don't set one specific speed value, for example 50. A symbolic value can represent the entire valid range at once.
It's not just the source text that needs to be checked.
For Sekura JS, we decided to check not only the source file, but also the compilation result.
Simplified, the chain looks like this:
program .sjs
↓
compiler
↓
executable object .sobj
↓
specification check .sjvThis is a fundamental decision.
If the verification were performed only relative to the source text, the compiler error could remain beyond the proof. When checking a machine object, the system examines exactly the code that is supposed to be executed on Memora8.
During the development process, this approach has already made it possible to detect a real compiler error: in one case, an ordinary global 32-bit variable was mistakenly treated as a pointer, which turned the arithmetic expression into another calculation.
Routine tests did not immediately identify this problem, and the formal contract showed a discrepancy between the expected and actual state transition.
One meaning of machine commands for modeling and proof
Here comes another important problem.
You can create one processor emulator and write a formal model of its commands separately. But if these two implementations diverge, we get two different versions of what the same machine instruction means.
Memora8 uses a different principle: the meaning of instructions should be determined by a common semantic basis.
That is, the same operation model is used for normal execution in the simulator and for symbolic execution in the proof.:
→→ normal execution
MR8 semantics
→→ symbolic verificationFor example, if addition, memory loading, or transition are defined, this meaning should not be independently described for each instrument.
This reduces the risk of a situation where the simulator considers one implementation to be correct, and the formal verification tool actually checks a slightly different machine.
Symbolic execution of machine code
A regular simulator gets specific numbers.:
r1 = 10
r2 = 20and calculates a specific result:
r3 = 30A symbolic check can instead get:
r1 = X
r2 = Ywhere X and Y represent the set of valid values.
Then the execution of the machine code generates not a specific result, but a mathematical expression.:
r3 = X + YTogether with the SJV conditions, this expression is passed to the solver, which tries to find a valid state in which the specified property is violated.
If such a state exists, we get a counterexample.
If it is proven that it does not exist in a given area, the property is considered confirmed for this model.
A counterexample is more important than an error message
A regular test usually reports:
expected 10
received 11A formal check can show much more.
It is able to find a specific initial state and input data in which the implementation violates the specification.:
function: add
input: ...
initial state: ...
condition violated: ...This turns formal verification into a fairly practical development tool.
If the specification is incorrect, a contradiction is found in the model itself. If the implementation is incorrect, a specific error path appears.
The result is SJP
After successful verification, a separate confirmation object is created — SJP.
His task is not just to say:
verifiedIt should be linked to specific input materials.:
source module
SJV specification
executable object
processor
version semantics
version dependency checking environmentHashes of the content are used for this purpose.
If you change the program or executable object, the previous verification result can no longer be automatically considered valid.
The same applies to changing the specification or semantics of the processor.
This way, the proof is tied not to the file name, but to its specific contents.
You can build a graph from the proofs.
The large program consists of modules.
It is almost impossible to formally verify the entire system every time, so a composition of evidence is necessary.
If a module uses another module, the verifying system may require confirmation of its contract.:
module A
↓
uses
↓
module B
↓
has its own SJPWhen checking module A, the specific confirmed result of module B is taken into account. The hash of this result is included in the new confirmation.
A graph is gradually being formed:
SJP A
├── SJP B
│ ├── SJP D
│ └── SJP E
└── SJP CIf you change module D, its confirmation will change. Then the dependent checks can be considered obsolete and performed anew.
This is one way to scale formal verification from a single function to a large system.
SJV can describe more than just Sekura JS
The same idea applies to the hardware.
The specification may refer to the Sekura JS program.:
module motor.sjsor a supported description of the digital circuit:
module top_level_cpu.svIn the latter case, the hardware implementation is already being checked.
This allows us to use one general idea.:
implementation
+
formal specification
↓
verification of complianceregardless of whether the implementation is a software module or a part of the processor.
Of course, digital circuits use their own semantics, and the supported subset of the hardware description language must be strictly defined.
Why can't you just check the entire SystemVerilog?
The complete language of description of digital circuits is very large. It contains designs designed not only for hardware synthesis, but also for modeling, testing, and complex development tools.
To support everything at once would mean dramatically increasing both the verifier itself and the trusted base.
Therefore, a limited subset is defined for SJV, which is really necessary to describe the testable parts of Memora8.
This is the same principle that is used in the processor itself: the limitation of capabilities is sometimes not a disadvantage, but a way to make the system visible.
If the system does not yet know how to check a certain construction correctly, the result should not be "proven", but:
not supportedor:
verification is not completedThis distinction is fundamentally important.
Successful test and proof — different results
In our system, the verification results are specifically separated.
The test can tell:
TEST PASSEDThis only means that a particular launch has produced the expected result.
The formal model can be correctly disassembled:
MODEL VERIFIEDBut this does not mean that the specific implementation corresponds to it.
Machine safety and compliance of the implementation with the contracts are checked separately.
If the solver failed to finish the proof, the result does not automatically turn into a successful one.:
VERIFICATION INCONCLUSIVEIf the design is still outside the supported model:
VERIFICATION UNSUPPORTEDWe consider this honesty of the result to be no less important than the proof itself.
What has already been tested on Sekura JS
The current SJV prototype is already being used not only on several artificial expressions.
One of the test examples contains six valid states and ten functions that move the system between these states and modify the data.
They are checked for it, in particular:
- allowed transitions between modes;
- saving values that should not change;
- arithmetic operations on the counter;
- correctness of the returned values;
- memory boundaries;
- memory card;
- stack and function call conventions.
For the correct specification, the implementation has received a positive result. An intentionally modified condition led to the discovery of a violation and a counterexample.
In the total set of tests, 41 out of 41 tests passed at the time of the recorded result.
This is not yet a proof of the whole Sekura JS, much less a proof of the entire system. But this is already a working chain from the source program to the symbolic execution of its machine code.
Where is Reganta OS here
Reganta is designed as a fairly small modular operating system for Memora8.
It does not have a classical process model and a separate heavy process scheduler. The main unit of execution is the Sekura JS module, and system requests are transmitted via messages.
The simplified scheme looks like this:
module
↓
system request
↓
queue
↓
main module Reganta
↓
solutionThe main system module can manage memory pages, change memory mapping, trigger page movement, and perform other privileged actions.
Such an architecture is interesting from the point of view of formal verification precisely because the main system transitions can be made explicit.
Instead of a large number of hidden states of the classical operating system, we are trying to get a limited set of modules and well-defined operations between them.
For example, page ownership
A rather specific property can be formulated for memory management.:
one physical page
cannot be
exclusively owned
by two independent owners at the same timeThen it is necessary to link several levels.
The decision to transfer the page is checked at the Reganta level.
At the machine code level, it is verified that the system module actually performs the permitted sequence of actions.
At the Memora8 level, it is checked that the hardware mechanisms of display and ownership do not allow circumventing the established rules.
Ideally, one system property is gradually traced down through the entire stack.
This is exactly what is much more interesting than separately proving several functions that are not connected by a common meaning.
The processor must also be part of the chain.
Even perfectly validated machine code is useless if the processor's hardware implementation executes it differently.
Therefore, the next level is the formal verification of Memora8 itself.
For example, for a separate command, you can specify:
state before
+
machine command
↓
state afterand prove that the digital circuit implements the same transition that architectural semantics sets.
More is needed for the pipeline: it needs to be shown that internal stages, delays, and redirects do not change the observed architectural behavior.
From the outside, the program should see the same machine that is described in the formal command model.
The result is a chain
If you gradually close these levels, the target structure looks something like this:
Sekura JS
↓
SJV
↓
proven machine object
↓
Reganta OS
↓
architectural semantics of Memora8
↓
proven hardware implementationBut arrows are more important than rectangles here.
It is necessary to prove not only the properties of each block, but also the correspondence between neighboring levels.
For example:
the meaning of the Sekura JS operation
=
the meaning of the resulting machine codeand further:
the meaning of the machine command
=
the behavior of the hardware implementationOtherwise, two independently proven components may still interact incorrectly with each other.
There is no complete proof yet.
It is important to accurately identify the current state.
We are not claiming that the entire Sekura JS — Reganta — Memora8 stack is formally proven. To date, only a part of this chain has been implemented and verified.
There is a working SJV check for the supported Sekura JS domain and the machine object. There is a single Memora8 semantics for regular and symbolic execution. It is becoming possible to apply the same approach to the hardware description of the processor.
Reganta is being designed with future verifiability in mind, but its full formal proof has not yet been completed.
In addition, there are limitations of symbolic execution, unsupported constructions, limitations of the solver and parts of the environment that still have to be trusted.
That is why it is important for us to keep the boundaries of each result obtained.
Why don't we try to prove everything at once
class="paragraph"> A complete modern computing stack contains millions of states, many devices, and a huge amount of software.
An attempt to formalize the entire system at once will almost certainly end up with an impractical model.
That's why we're going in the opposite direction: we're trying to make the stack itself smaller.
A small set of processor instructions, an explicit memory model, a limited number of system device types, a compact operating system, and a system language with predictable semantics reduce the number of hidden states.
In other words, verifiability becomes not an additional feature after the completion of development, but one of the requirements for the architecture itself.
Trust should become measurable
Today, we often trust a computing system because its components are widely used, have passed many tests, and have been in operation for a long time.
These are valuable reasons for trust, but they do not answer the question of which properties are guaranteed.
Formal verification allows us to proceed to a more precise formulation.:
this version of the program
on this version of the machine model
with these prerequisites
satisfies these propertiesIf anything significant has changed, the check needs to be reviewed.
In this way, trust ceases to be just a general sense of reliability and gradually turns into a set of specific verifiable statements.
Why do we need the entire stack?
For us, SJV is not interesting as a separate program verification tool.
If the task consisted only in proving several algorithms, the existing means of formal methods would be sufficient.
The research question is much broader: is it possible to build a computing platform so that verifiability passes through all its main levels?
Sekura JS provides the source program. SJV sets its properties. The machine object is being checked. Reganta tries to make system transitions explicit. Memora8 provides a small architectural model, and its hardware description is also gradually entering the field of verification.
This is not yet a complete proven stack, but a development direction.
But if this approach can be completed, the result will not just be another processor or another operating system. A computing environment will appear in which, for critical parts, it is possible to trace the chain from the properties of the program to the behavior of the hardware and specify exactly what has been proven, what assumptions the proof is based on, and what still has to be trusted.
Формально проверить отдельную функцию значительно проще, чем целую вычислительную систему. Даже если доказано, что исходная программа выполняет нужное свойство, между ней и реальным результатом остаются компилятор, машинный код, операционная система и процессор.
Каждый такой уровень может изменить поведение системы или добавить собственную ошибку. Поэтому для Memora8 мы исследуем более широкую задачу: можно ли связать проверку программы, машинного кода, операционной системы и процессора в одну последовательную цепочку?
Именно для этого рядом с языком Sekura JS развивается система формальных спецификаций SJV, процессор Memora8 и операционная система Reganta.
Цель состоит не в том, чтобы однажды поставить на всю систему штамп «доказано». Намного важнее точно знать, какие свойства проверены, относительно какой реализации они доказаны и где остаются границы доверия.
Почему доказательства отдельных компонентов недостаточно
Представим, что мы доказали корректность некоторой функции на уровне исходного языка:
исходная программа
↓
свойство доказаноНо затем эту программу преобразует компилятор:
исходная программа
↓
компилятор
↓
машинный кодЕсли компилятор допустил ошибку, доказанное свойство исходной программы уже не гарантирует корректность исполняемого кода.
Дальше машинный код выполняется процессором:
машинный код
↓
процессорЕсли процессор реализует одну из команд не так, как предполагает модель языка, возникает ещё один разрыв.
Между ними также находится операционная система, которая управляет памятью, доступом к устройствам и системными действиями.
В итоге реальная цепочка выглядит намного длиннее:
исходная программа
↓
компилятор
↓
машинная программа
↓
операционная система
↓
процессор
↓
аппаратные устройстваПоэтому проверка только первого звена оставляет слишком много предположений относительно всех последующих.
Идея SJV: отделить программу от её свойств
В системе Sekura программа и её формальная спецификация существуют отдельно.
Например:
motor.sjs
motor.sjvФайл Sekura JS содержит реализацию, а SJV описывает свойства, которым эта реализация должна соответствовать.
Это важное разделение. Мы не пытаемся считать сам программный код его собственным доказательством. Спецификация задаётся отдельно и может, например, описывать допустимые состояния устройства:
режим = работа
скорость < 100
ошибка = 0или другое допустимое состояние:
режим = авария
скорость = 0
двигатель отключёнТаким образом, SJV описывает не последовательность команд, а границы допустимого поведения.
Проверяется состояние до и после действия
Для отдельной функции можно задавать условия на состояние до её выполнения и после него.
Например, операция изменения скорости может иметь следующий смысл:
до выполнения:
новая скорость < 100
после выполнения:
скорость = новое значениеВ SJV значения после выполнения обозначаются отдельно от исходного состояния. Благодаря этому спецификация описывает переход:
состояние до
↓
операция
↓
состояние послеПроверяющая система должна установить, что реальная реализация функции действительно приводит только к таким состояниям, которые разрешены спецификацией.
Это уже отличается от обычного теста. Мы не задаём одно конкретное значение скорости, например 50. Символическое значение может представлять весь допустимый диапазон сразу.
Проверять нужно не только исходный текст
Для Sekura JS мы решили проверять не только исходный файл, но и результат компиляции.
Упрощённо цепочка выглядит так:
программа .sjs
↓
компилятор
↓
исполняемый объект .sobj
↓
проверка по спецификации .sjvЭто принципиальное решение.
Если бы проверка выполнялась только относительно исходного текста, ошибка компилятора могла бы остаться за пределами доказательства. При проверке машинного объекта система исследует именно тот код, который предполагается выполнять на Memora8.
В процессе разработки такой подход уже позволил обнаружить реальную ошибку компилятора: обычная глобальная 32-битная переменная в одном случае ошибочно обрабатывалась как указатель, из-за чего арифметическое выражение превращалось в другое вычисление.
Обычные тесты эту проблему не выявили сразу, а формальный контракт показал расхождение между ожидаемым и фактическим переходом состояния.
Один смысл машинных команд для моделирования и доказательства
Здесь появляется ещё одна важная проблема.
Можно создать один эмулятор процессора и отдельно написать формальную модель его команд. Но если эти две реализации расходятся, мы получаем две разные версии того, что означает одна и та же машинная команда.
В Memora8 используется другой принцип: смысл инструкций должен определяться общей семантической основой.
То есть одна и та же модель операции используется для обычного выполнения в симуляторе и для символического исполнения при доказательстве:
┌→ обычное выполнение
семантика MR8
└→ символическая проверкаНапример, если определено, как работает сложение, загрузка из памяти или переход, этот смысл не должен заново независимо описываться для каждого инструмента.
Это уменьшает риск ситуации, когда симулятор считает одну реализацию правильной, а средство формальной проверки фактически проверяет немного другую машину.
Символическое выполнение машинного кода
Обычный симулятор получает конкретные числа:
r1 = 10
r2 = 20и вычисляет конкретный результат:
r3 = 30Символическая проверка вместо этого может получить:
r1 = X
r2 = Yгде X и Y представляют множество допустимых значений.
Затем выполнение машинного кода порождает не конкретный результат, а математическое выражение:
r3 = X + YВместе с условиями SJV это выражение передаётся решателю, который пытается найти такое допустимое состояние, при котором заданное свойство нарушится.
Если такое состояние находится, мы получаем контрпример.
Если доказано, что его не существует в заданной области, свойство считается подтверждённым для этой модели.
Контрпример важнее сообщения об ошибке
Обычный тест обычно сообщает:
ожидалось 10
получено 11Формальная проверка может показать значительно больше.
Она способна найти конкретное исходное состояние и входные данные, при которых реализация нарушает спецификацию:
функция: add
вход: ...
начальное состояние: ...
нарушено условие: ...Это превращает формальную проверку в достаточно практический инструмент разработки.
Если спецификация неверна, обнаруживается противоречие в самой модели. Если неверна реализация, появляется конкретный путь к ошибке.
Результатом становится SJP
После успешной проверки создаётся отдельный объект подтверждения — SJP.
Его задача не просто сказать:
провереноОн должен быть связан с конкретными входными материалами:
исходный модуль
спецификация SJV
исполняемый объект
версия процессора
версия семантики
окружение проверки
зависимостиДля этого используются хеши содержимого.
Если изменить программу или исполняемый объект, прежний результат проверки больше нельзя автоматически считать действующим.
То же самое относится к изменению спецификации или семантики процессора.
Так доказательство привязывается не к названию файла, а к его конкретному содержимому.
Из доказательств можно строить граф
Большая программа состоит из модулей.
Пытаться каждый раз формально проверять всю систему целиком практически невозможно, поэтому необходима композиция доказательств.
Если модуль использует другой модуль, проверяющая система может потребовать подтверждение его контракта:
модуль A
↓
использует
↓
модуль B
↓
имеет собственный SJPПри проверке модуля A учитывается конкретный подтверждённый результат модуля B. Хеш этого результата включается в новое подтверждение.
Постепенно образуется граф:
SJP A
├── SJP B
│ ├── SJP D
│ └── SJP E
└── SJP CЕсли изменить модуль D, изменится его подтверждение. Тогда зависимые проверки можно признать устаревшими и выполнить заново.
Это один из способов масштабировать формальную проверку от отдельной функции к большой системе.
SJV может описывать не только Sekura JS
Та же идея применяется и к аппаратной части.
Спецификация может ссылаться на программу Sekura JS:
module motor.sjsили на поддерживаемое описание цифровой схемы:
module top_level_cpu.svВ последнем случае проверяется уже аппаратная реализация.
Это позволяет использовать одну общую идею:
реализация
+
формальная спецификация
↓
проверка соответствиянезависимо от того, является реализация программным модулем или частью процессора.
Конечно, для цифровых схем используется собственная семантика, а поддерживаемое подмножество языка аппаратного описания должно быть строго определено.
Почему нельзя просто проверить весь SystemVerilog
Полный язык описания цифровых схем очень велик. Он содержит конструкции, предназначенные не только для синтеза аппаратуры, но и для моделирования, тестирования и сложных средств разработки.
Поддержать всё сразу означало бы резко увеличить как сам верификатор, так и доверенную основу.
Поэтому для SJV определяется ограниченное подмножество, которое действительно необходимо для описания проверяемых частей Memora8.
Это тот же принцип, который используется и в самом процессоре: ограничение возможностей иногда является не недостатком, а способом сделать систему обозримой.
Если некоторую конструкцию система пока не умеет корректно проверять, результат должен быть не «доказано», а:
не поддерживаетсяили:
проверка не завершенаТакое различие принципиально важно.
Успешный тест и доказательство — разные результаты
В нашей системе результаты проверки специально разделяются.
Тест может сказать:
TEST PASSEDЭто означает только то, что конкретный запуск дал ожидаемый результат.
Формальная модель может быть корректно разобрана:
MODEL VERIFIEDНо это ещё не означает, что конкретная реализация ей соответствует.
Отдельно проверяется машинная безопасность и соответствие реализации контрактам.
Если решателю не удалось закончить доказательство, результат не превращается автоматически в успешный:
VERIFICATION INCONCLUSIVEЕсли конструкция пока находится за пределами поддерживаемой модели:
VERIFICATION UNSUPPORTEDМы считаем такую честность результата не менее важной, чем само доказательство.
Что уже было проверено на Sekura JS
Текущий прототип SJV уже используется не только на нескольких искусственных выражениях.
Один из проверочных примеров содержит шесть допустимых состояний и десять функций, которые переводят систему между этими состояниями и изменяют данные.
Для него проверяются, в частности:
- разрешённые переходы между режимами;
- сохранение значений, которые не должны изменяться;
- арифметические операции над счётчиком;
- корректность возвращаемых значений;
- границы памяти;
- карта памяти;
- стек и соглашения вызова функций.
Для правильной спецификации реализация получила положительный результат. Намеренно изменённое условие привело к обнаружению нарушения и контрпримеру.
В общем наборе тестов на момент зафиксированного результата прошёл 41 тест из 41.
Это ещё не доказательство всего Sekura JS и тем более не доказательство всей системы. Но это уже работающая цепочка от исходной программы до символического исполнения её машинного кода.
Где здесь Reganta OS
Reganta проектируется как достаточно небольшая модульная операционная система для Memora8.
В ней нет классической модели процессов и отдельного тяжёлого планировщика процессов. Основной единицей исполнения является модуль Sekura JS, а системные запросы передаются через сообщения.
Упрощённая схема выглядит так:
модуль
↓
системный запрос
↓
очередь
↓
основной модуль Reganta
↓
решениеОсновной системный модуль может управлять страницами памяти, изменять отображение памяти, запускать перемещение страниц и выполнять другие привилегированные действия.
Такая архитектура интересна с точки зрения формальной проверки именно потому, что основные системные переходы можно сделать явными.
Вместо большого количества скрытых состояний классической операционной системы мы пытаемся получить ограниченный набор модулей и хорошо определённых операций между ними.
Например, владение страницей
Для управления памятью можно сформулировать достаточно конкретное свойство:
одна физическая страница
не может одновременно
исключительно принадлежать
двум независимым владельцамТогда необходимо связать несколько уровней.
На уровне Reganta проверяется решение о передаче страницы.
На уровне машинного кода проверяется, что системный модуль действительно выполняет разрешённую последовательность действий.
На уровне Memora8 проверяется, что аппаратные механизмы отображения и владения не позволяют обойти установленные правила.
В идеальном случае одно системное свойство постепенно прослеживается вниз через весь стек.
Именно это намного интереснее, чем отдельно доказать несколько функций, не связанных общим смыслом.
Процессор тоже должен входить в цепочку
Даже идеально проверенный машинный код бесполезен, если аппаратная реализация процессора выполняет его иначе.
Поэтому следующий уровень — формальная проверка самого Memora8.
Например, для отдельной команды можно задать:
состояние до
+
машинная команда
↓
состояние послеи доказать, что цифровая схема реализует тот же переход, который задаёт архитектурная семантика.
Для конвейера требуется больше: необходимо показать, что внутренние стадии, задержки и перенаправления не меняют наблюдаемое архитектурное поведение.
Снаружи программа должна видеть ту же машину, которая описана в формальной модели команд.
В результате получается цепочка
Если постепенно закрывать эти уровни, целевая структура выглядит примерно так:
Sekura JS
↓
SJV
↓
проверенный машинный объект
↓
Reganta OS
↓
архитектурная семантика Memora8
↓
проверенная аппаратная реализацияНо стрелки здесь важнее прямоугольников.
Нужно доказать не только свойства каждого блока, но и соответствие между соседними уровнями.
Например:
смысл операции Sekura JS
=
смысл полученного машинного кодаи далее:
смысл машинной команды
=
поведение аппаратной реализацииИначе два независимо доказанных компонента всё равно могут неправильно взаимодействовать друг с другом.
Полного доказательства пока нет
Важно точно обозначить текущее состояние.
Мы не утверждаем, что весь стек Sekura JS — Reganta — Memora8 формально доказан. На сегодняшний день реализована и проверяется только часть этой цепочки.
Есть работающая проверка SJV для поддерживаемой области Sekura JS и машинного объекта. Есть единая семантика Memora8 для обычного и символического исполнения. Развивается возможность применять тот же подход к аппаратному описанию процессора.
Reganta проектируется с учётом будущей проверяемости, но её полное формальное доказательство ещё не выполнено.
Кроме того, существуют ограничения символического исполнения, неподдерживаемые конструкции, ограничения решателя и части окружения, которым пока приходится доверять.
Именно поэтому для нас важно сохранять границы каждого полученного результата.
Почему мы не пытаемся доказать всё сразу
Полный современный вычислительный стек содержит миллионы состояний, множество устройств и огромное количество программного обеспечения.
Попытка сразу формализовать всю такую систему почти наверняка закончится непрактичной моделью.
Поэтому мы идём в противоположном направлении: стараемся сделать сам стек меньше.
Небольшой набор команд процессора, явная модель памяти, ограниченное число типов системных устройств, компактная операционная система и системный язык с предсказуемой семантикой уменьшают количество скрытых состояний.
То есть проверяемость становится не дополнительной функцией после завершения разработки, а одним из требований к самой архитектуре.
Доверие должно становиться измеримым
Сегодня мы часто доверяем вычислительной системе потому, что её компоненты широко используются, прошли множество тестов и давно находятся в эксплуатации.
Это ценные основания для доверия, но они плохо отвечают на вопрос, какие именно свойства гарантируются.
Формальная верификация позволяет перейти к более точной формулировке:
эта версия программы
на этой версии машинной модели
при этих предпосылках
удовлетворяет этим свойствамЕсли изменилось что-либо существенное, проверку необходимо пересмотреть.
Так доверие перестаёт быть только общим ощущением надёжности и постепенно превращается в набор конкретных проверяемых утверждений.
Зачем нужен весь стек
Для нас SJV интересен не как отдельное средство проверки программ.
Если бы задача заключалась только в доказательстве нескольких алгоритмов, существующих средств формальных методов было бы достаточно.
Исследовательский вопрос гораздо шире: можно ли построить вычислительную платформу так, чтобы проверяемость проходила через все её основные уровни?
Sekura JS даёт исходную программу. SJV задаёт её свойства. Проверяется машинный объект. Reganta старается сделать системные переходы явными. Memora8 предоставляет небольшую архитектурную модель, а его аппаратное описание также постепенно входит в область проверки.
Это пока не завершённый доказанный стек, а направление разработки.
Но если такой подход удастся довести до конца, результатом будет не просто ещё один процессор или ещё одна операционная система. Появится вычислительная среда, в которой для критически важных частей можно проследить цепочку от свойства программы до поведения аппаратуры и точно указать, что доказано, на каких предположениях основано доказательство и чему всё ещё приходится доверять.
Share
