The post has been translated automatically. Original language: Russian
A formally proven program does not guarantee the correct operation of the entire system.
The reason is simple: the processor usually does not execute the source code directly.
There are several intermediate levels between the program and the hardware:
the source code
, the compiler
, machine code
, operating system
↓
processorEach of them affects the final result.
Therefore, verification of the program naturally leads to a broader issue.:
can the entire execution chain be trusted?
What does the compiler do?
The compiler converts a program written in a high-level language into processor instructions.
Simplified:
the original program
, the compiler
↓
machine codeAt the same time, the compiler performs many transformations.:
- changes the representation of expressions;
- allocates registers;
- rebuilds calculations;
- optimizes cycles;
- removes unnecessary operations;
- changes the order of instructions where it considers it acceptable.
It is expected that after all the transformations, the meaning of the program will remain.
However, the compiler itself is a complex software product and may also contain errors.
Where the problem occurs
Suppose the properties of the original program are proven.
But then an erroneous optimization turns it into another machine code.
It turns out an unpleasant situation:
the source program is correct
, the machine code is no longer thereIn this case, the proof of the source text does not automatically extend to the executable result.
Therefore, it is necessary to establish a link between the two levels.:
The machine code must preserve the behavior of the source program within a given model.
This is already the task of verifying the compiler or the compilation result.
Why is compiler verification especially important?
One user program can be used in one product.
The compiler transforms thousands and millions of programs.
An error in such a tool can affect a large number of systems at once.
Therefore, the proof of compilation correctness is of particular value.:
the correct program
↓
correct conversion
↓
equivalent machine codeThe more reliable this transition is, the less you have to rely on the assumption "the compiler probably did everything right."
After the compiler, the operating system appears
Even correct machine code usually does not work in isolation.
The operating system manages the execution environment.
She is responsible for:
- memory;
- processes;
- access rights;
- switching tasks;
- devices;
- interruptions;
- file resources;
- interaction between programs.
Many of the application's properties are based on assumptions about how the OS works.
For example:
the memory area of the process
is inaccessible to other processesIf this condition is violated, the application may lose its security properties, even if its own code is written without errors.
You don't need to verify everything at once
Modern universal operating systems are extremely complex.
Therefore, an attempt to prove absolutely all their properties at once is almost impossible.
One of the engineering approaches is to reduce the critical part of the system.
For example:
A small core
↓
memory
↓
Isolation
, access rights
For a compact kernel, it is easier to precisely define the behavior and prove the key properties.
The rest of the functionality may be outside the minimum trusted part.
What is a trusted computing base?
For any system, there is a set of components on which the validity of its guarantees depends.
It is called a trusted computing base.
If the security of the application depends on:
the compiler
OS kernels
processor memory mechanismthen an error in any of these components potentially destroys the properties of the system above.
Therefore, one of the goals of formal verification is to make the trusted database as small and understandable as possible.
You don't have to prove the whole world.
It is important to understand:
- What we trust;
- What we have proved;
- what assumptions are the guarantees based on?
Chain of evidence
Ideally, the layers of a computing system are connected sequentially.:
program specification
, source code
, machine code
, operating system kernel
, Processor architectureEach transition requires its own compliance statement.
For example:
the source code
conforms to the specificationthen:
the machine code
preserves the behavior of the source codeand for the operating system:
the runtime
retains the required isolation
and access rulesThis is how not one large proof is formed, but a set of related guarantees.
Architecture becomes part of the task
The more components and hidden states a system contains, the more difficult it is to build such evidence.
Therefore, formal verification affects architectural decisions.
A system designed for verification usually tends to:
- a smaller trusted database;
- simple interfaces;
- clear responsibilities of the components;
- the minimum amount of implicit behavior;
- a controlled number of states.
In other words, provability cannot be fully added at the end of development.
It is more convenient to embed it in the very structure of the system.
Where does the program part end?
After the program, the compiler, and the operating system, there remains one more fundamental component.
The processor receives machine instructions and changes the state of the computer:
- registers;
- memory;
- execution modes;
- the status of the devices.
If the hardware implementation of the instruction differs from the expected one, the guarantees of the upper levels are again in question.
Now the chain looks like this:
program
, the compiler
, operating system
↓
machine instructions
↓
processorTherefore, the next step is already beyond the limits of conventional software.
Is it possible to mathematically prove the correctness of the processor itself?
Формально доказанная программа ещё не гарантирует правильную работу всей системы.
Причина проста: процессор обычно не выполняет исходный код напрямую.
Между программой и аппаратурой есть несколько промежуточных уровней:
исходный код
↓
компилятор
↓
машинный код
↓
операционная система
↓
процессорКаждый из них влияет на конечный результат.
Поэтому верификация программы естественно приводит к более широкому вопросу:
можно ли доверять всей цепочке исполнения?
Что делает компилятор
Компилятор преобразует программу, написанную на языке высокого уровня, в инструкции процессора.
Упрощённо:
исходная программа
↓
компилятор
↓
машинный кодПри этом компилятор выполняет множество преобразований:
- меняет представление выражений;
- распределяет регистры;
- перестраивает вычисления;
- оптимизирует циклы;
- удаляет лишние операции;
- изменяет порядок инструкций там, где считает это допустимым.
Ожидается, что после всех преобразований смысл программы сохранится.
Однако компилятор сам является сложным программным продуктом и тоже может содержать ошибки.
Где возникает проблема
Предположим, свойства исходной программы доказаны.
Но затем ошибочная оптимизация превращает её в другой машинный код.
Получается неприятная ситуация:
исходная программа — корректна
машинный код — уже нетДоказательство исходного текста в таком случае не распространяется автоматически на исполняемый результат.
Следовательно, требуется установить связь между двумя уровнями:
машинный код должен сохранять поведение исходной программы в рамках заданной модели.
Это уже задача верификации компилятора или результата компиляции.
Почему проверка компилятора особенно важна
Одна пользовательская программа может использоваться в одном продукте.
Компилятор же преобразует тысячи и миллионы программ.
Ошибка в таком инструменте способна влиять сразу на большое количество систем.
Поэтому доказательство корректности компиляции имеет особую ценность:
правильная программа
↓
корректное преобразование
↓
эквивалентный машинный кодЧем надёжнее этот переход, тем меньше приходится полагаться на предположение «компилятор, скорее всего, всё сделал правильно».
После компилятора появляется операционная система
Даже корректный машинный код обычно работает не изолированно.
Операционная система управляет средой его выполнения.
Она отвечает за:
- память;
- процессы;
- права доступа;
- переключение задач;
- устройства;
- прерывания;
- файловые ресурсы;
- взаимодействие между программами.
Многие свойства приложения основаны на предположениях о работе ОС.
Например:
область памяти процесса
недоступна другим процессамЕсли это условие нарушается, приложение может потерять свойства безопасности, даже если его собственный код написан без ошибок.
Верифицировать нужно не всё сразу
Современные универсальные операционные системы чрезвычайно сложны.
Поэтому попытка доказать абсолютно все их свойства сразу практически непосильна.
Один из инженерных подходов состоит в уменьшении критической части системы.
Например:
небольшое ядро
↓
память
↓
изоляция
↓
права доступаДля компактного ядра легче точно задать поведение и доказать ключевые свойства.
Остальная функциональность может находиться за пределами минимальной доверенной части.
Что такое доверенная вычислительная база
Для любой системы существует набор компонентов, от которых зависит истинность её гарантий.
Его называют доверенной вычислительной базой.
Если безопасность приложения зависит от:
компилятора
ядра ОС
механизма памяти
процессорато ошибка в любом из этих компонентов потенциально разрушает свойства системы выше.
Поэтому одна из целей формальной верификации — сделать доверенную базу как можно меньше и понятнее.
Не обязательно доказывать весь мир.
Важно понимать:
- чему мы доверяем;
- что мы доказали;
- на каких предположениях основаны гарантии.
Цепочка доказательств
В идеале уровни вычислительной системы связываются последовательно:
спецификация программы
↓
исходный код
↓
машинный код
↓
ядро операционной системы
↓
архитектура процессораДля каждого перехода требуется своё утверждение о соответствии.
Например:
исходный код
соответствует спецификациизатем:
машинный код
сохраняет поведение исходного кодаа для операционной системы:
среда выполнения
сохраняет требуемую изоляцию
и правила доступаТак формируется не одно большое доказательство, а набор связанных гарантий.
Архитектура становится частью задачи
Чем больше компонентов и скрытых состояний содержит система, тем труднее строить такие доказательства.
Поэтому формальная верификация влияет на архитектурные решения.
Система, рассчитанная на верификацию, обычно стремится к:
- меньшей доверенной базе;
- простым интерфейсам;
- чётким обязанностям компонентов;
- минимальному количеству неявного поведения;
- контролируемому числу состояний.
Иными словами, доказуемость нельзя полностью добавить в конце разработки.
Её удобнее закладывать в саму структуру системы.
Где заканчивается программная часть
После программы, компилятора и операционной системы остаётся ещё один фундаментальный компонент.
Процессор получает машинные инструкции и изменяет состояние компьютера:
- регистры;
- память;
- режимы исполнения;
- состояние устройств.
Если аппаратная реализация инструкции отличается от ожидаемой, гарантии верхних уровней снова оказываются под вопросом.
Теперь цепочка выглядит так:
программа
↓
компилятор
↓
операционная система
↓
машинные инструкции
↓
процессорПоэтому следующий шаг уже выходит за пределы обычного программного обеспечения.
Можно ли математически доказать правильность самого процессора?
Share
