The post has been translated automatically. Original language: Russian
Rust and Sekura JS relate to system programming, but they approach the reliability of programs from different angles. Therefore, it would not be entirely correct to compare them only by syntax, speed, or set of features.
Rust strives to prevent entire classes of errors even at the compilation stage. Sekura JS is created with another main purpose: to obtain a software layer, the machine result of which can be included in formal verification along with the Memora8 architecture and other system components.
Both approaches are aimed at improving reliability, but they solve different tasks.
What problem does Rust solve?
One of the well—known features of Rust is strict memory management. The compiler monitors the lifetime of values, data ownership, and access rules.
This approach allows you to detect many errors before running the program. For example, the language helps to prevent the use of already freed memory or dangerous simultaneous access to mutable data.
Much of this protection is built directly into the language rules and is checked by the compiler.
This is an important property for system programming: the developer retains low-level control, but receives additional guarantees even during the program build.
Sekura JS comes from a different task
In Sekura JS, memory remains explicit. The language uses pointers, arrays, structures, and integer values of various sizes.
This is not done because memory errors are not important. The reason is the different architecture of the project.
Sekura JS is created as part of the Sekura hardware and software stack, where it is necessary to be able to verify the specific behavior of the already received machine code.
That is, the main question sounds not only like this:
"can a language ban a dangerous program in advance?"
A second question is added:
"does the machine code actually created meet the specified formal requirement?"
Checking the language and checking the result are not the same thing.
The type system may prohibit a certain erroneous construction even before the program is started. This is a powerful way to increase reliability.
But such a check is not equal to proving an arbitrary property of the program.
For example, a function should maintain a certain limit for any acceptable input values, change only one area of the state, or transfer the system only between allowed states.
These properties no longer depend solely on the safety of memory management.
They need to formulate separately what the correct behavior should be, and check the implementation regarding this requirement.
This is the direction in which Sekura JS' approach is directed.
What is checked in Sekura JS
The Sekura JS source program is compiled into a SOBJ machine object for the Memora8 architecture.
A formal description of SJV is given separately. It allows you to define acceptable initial states and requirements for the state after the function is executed.
After that, SJV analyzes the machine code and checks whether its behavior corresponds to the specified condition.
This is an important feature of the approach: the object of verification is not only the source code of the program, but also the actual result of the compiler.
If the compiler has created an incorrect sequence of machine instructions, a formal check may detect a discrepancy with the requirement.
Why is this a different line of trust
When using strict language rules, a significant part of the trust is transferred to the compiler itself and the correctness of the implementation of these rules.
In Sekura JS, we are trying to further check what happened after compilation.
The source program may look correct, but the final behavior of the processor is determined by machine instructions. Therefore, the ability to verify SOBJ allows you to bring the proof closer to the code that really needs to be executed.
This does not eliminate all trusted components. The verification tool, the processor instruction model, and the transformation of conditions into a mathematical problem should also be considered separately.
But the area between the source program and the machine result becomes more observable.
Memory security remains a separate property.
Formal verification does not mean automatic memory security.
If a specific requirement describes only the arithmetic result of a function, it cannot be concluded from a successful check that all memory accesses in the entire program are safe.
The necessary properties must be included in the model being tested.
This is one of the important differences between the approaches.
Rust tries to make a certain class of errors impossible or significantly difficult at the level of the language itself. In Sekura JS, the checked property is explicitly set and confirmed relative to a specific machine result.
Therefore, one approach should not be considered a simple substitute for the other.
Simplicity of the Sekura JS model
Sekura JS uses a relatively small and explicit language model.
It is closely related to the Memora8 32-bit architecture. The language defines integer types of 8, 16, and 32 bits, explicit memory, pointers, arrays, structures, and functions.
The language does not try to hide the machine architecture behind a large runtime environment.
This is important for formal verification. The easier it is to establish a relationship between the initial operation and the state of the machine, the easier it is to formulate and verify specific properties.
Rust solves a broader problem and is designed for a large number of architectures and applications. Therefore, its language model is much richer.
What happens to compiler errors?
Even a strict language requires a valid compiler.
If the source program is valid, but the compiler mistakenly converted it to machine code, the properties of the source program alone do not guarantee the correctness of the result.
This is why verification of compilation results is being developed in Sekura JS.
Programs and formal conditions are created for individual requirements. Then the machine object obtained by the real compiler is checked.
If the compiler is changed, the same set of requirements can be checked again.
Thus, the evidence base refers to a specific version of the result, and not just to the rules of the source language.
An example of the difference in approaches
Let's imagine a function that modifies a counter.
At the language level, you can control the correctness of types and the permissibility of memory operations.
However, there may be additional requirements for a particular system: the counter must change strictly by a preset value, the other state must not change, and under certain conditions the result must remain in the set range.
Such properties are already the requirements of the system itself.
In Sekura JS, they can be described by a separate formal condition and checked against the compiled machine code.
"Therefore, "formal verification" is concerned not only with the question "is the language design safe", but also with the question "does the program implement the required behavior".
Why is Sekura JS not a replacement for Rust
Rust is a mature general—purpose language with a well-developed ecosystem and support for multiple platforms. It is suitable for a wide range of tasks where performance, system control and protection against many memory errors are required.
Sekura JS has a significantly narrower scope.
It is being developed together with Memora8, Reganta and Sekura formal verification tools. Its device is determined by the tasks of this software and hardware stack.
Therefore, the goal of the project is not to offer an alternative to Rust for all existing system programs.
Two different paths to reliability
The difference between Rust and Sekura JS shows well that the word "reliability" can mean different things.
One way is to make the language such that it does not allow the use of many dangerous constructs during compilation.
Another way is to make it possible to explicitly formulate the required property and verify that the specific machine code actually corresponds to it.
In practice, these ideas do not contradict each other. Strict rules of language and formal proofs can complement each other.
For Sekura JS, the main focus now is the second: link the source program, the compilation result, and the formal requirement so that the properties of the machine code can be checked in a reproducible way.
That is why the comparison with Rust is interesting for us not as a competition between two languages, but as a comparison of two different ways to increase trust in system software.
Rust и Sekura JS относятся к системному программированию, но подходят к надёжности программ с разных сторон. Поэтому сравнивать их только по синтаксису, скорости или набору возможностей было бы не совсем правильно.
Rust стремится предотвращать целые классы ошибок ещё на этапе компиляции. Sekura JS создаётся с другой основной целью: получить программный слой, машинный результат которого можно включить в формальную проверку вместе с архитектурой Memora8 и другими компонентами системы.
Оба подхода направлены на повышение надёжности, но решают разные задачи.
Какую проблему решает Rust
Одна из известных особенностей Rust — строгий контроль работы с памятью. Компилятор следит за временем жизни значений, владением данными и правилами доступа к ним.
Такой подход позволяет обнаруживать многие ошибки до запуска программы. Например, язык помогает предотвратить использование уже освобождённой памяти или опасный одновременный доступ к изменяемым данным.
Значительная часть такой защиты встроена непосредственно в правила языка и проверяется компилятором.
Для системного программирования это важное свойство: разработчик сохраняет низкоуровневый контроль, но получает дополнительные гарантии ещё во время сборки программы.
Sekura JS исходит из другой задачи
В Sekura JS память остаётся явной. Язык использует указатели, массивы, структуры и целочисленные значения разных размеров.
Это сделано не потому, что ошибки памяти не важны. Причина в другой архитектуре проекта.
Sekura JS создаётся как часть программно-аппаратного стека Sekura, где необходимо иметь возможность проверять конкретное поведение уже полученного машинного кода.
То есть основной вопрос звучит не только так:
«может ли язык заранее запретить опасную программу?»
Добавляется второй вопрос:
«соответствует ли фактически созданный машинный код заданному формальному требованию?»
Проверка языка и проверка результата — не одно и то же
Система типов может запретить определённую ошибочную конструкцию ещё до запуска программы. Это сильный способ повысить надёжность.
Но такая проверка не равна доказательству произвольного свойства программы.
Допустим, функция должна при любых допустимых входных значениях сохранять определённый предел, менять только одну область состояния или переводить систему только между разрешёнными состояниями.
Эти свойства зависят уже не только от безопасности обращения с памятью.
Для них требуется отдельно сформулировать, каким должно быть правильное поведение, и проверить реализацию относительно этого требования.
Именно в эту сторону направлен подход Sekura JS.
Что проверяется в Sekura JS
Исходная программа Sekura JS компилируется в машинный объект SOBJ для архитектуры Memora8.
Отдельно задаётся формальное описание SJV. В нём можно определить допустимые исходные состояния и требования к состоянию после выполнения функции.
После этого SJV анализирует уже машинный код и проверяет, соответствует ли его поведение заданному условию.
Это важная особенность подхода: объектом проверки является не только исходный текст программы, но и фактический результат работы компилятора.
Если компилятор создал неправильную последовательность машинных инструкций, формальная проверка может обнаружить расхождение с требованием.
Почему это другая граница доверия
При использовании строгих правил языка значительная часть доверия переносится на сам компилятор и правильность реализации этих правил.
В Sekura JS мы пытаемся дополнительно проверить то, что произошло после компиляции.
Исходная программа может выглядеть правильно, однако конечное поведение процессора определяется уже машинными инструкциями. Поэтому возможность проверить SOBJ позволяет приблизить доказательство к тому коду, который действительно должен исполняться.
Это не устраняет все доверенные компоненты. Средство проверки, модель команд процессора и преобразование условий в математическую задачу тоже должны рассматриваться отдельно.
Но область между исходной программой и машинным результатом становится более наблюдаемой.
Безопасность памяти остаётся отдельным свойством
Формальная проверка не означает автоматическую безопасность памяти.
Если конкретное требование описывает только арифметический результат функции, из успешной проверки нельзя сделать вывод, что все обращения к памяти во всей программе безопасны.
Необходимые свойства должны быть включены в проверяемую модель.
В этом и состоит одно из важных различий подходов.
Rust старается сделать определённый класс ошибок невозможным или существенно затруднённым на уровне самого языка. В Sekura JS проверяемое свойство задаётся явно и подтверждается относительно конкретного машинного результата.
Поэтому один подход не следует считать простой заменой другого.
Простота модели Sekura JS
Sekura JS использует сравнительно небольшую и явную модель языка.
Он тесно связан с 32-разрядной архитектурой Memora8. В языке определены целочисленные типы размером 8, 16 и 32 бита, явная память, указатели, массивы, структуры и функции.
Язык не пытается скрыть машинную архитектуру за большой средой исполнения.
Это важно для формальной проверки. Чем проще установить связь между исходной операцией и состоянием машины, тем легче формулировать и проверять конкретные свойства.
Rust решает более широкую задачу и предназначен для большого количества архитектур и областей применения. Поэтому его языковая модель значительно богаче.
Что происходит с ошибками компилятора
Даже строгий язык требует корректного компилятора.
Если исходная программа допустима, но компилятор ошибочно преобразовал её в машинный код, свойства исходной программы сами по себе не гарантируют правильность результата.
В Sekura JS именно поэтому развивается проверка результатов компиляции.
Для отдельных требований создаются программы и формальные условия. Затем проверяется машинный объект, полученный реальным компилятором.
При изменении компилятора тот же набор требований можно проверить повторно.
Таким образом, доказательная база относится к конкретной версии результата, а не только к правилам исходного языка.
Пример различия подходов
Представим функцию, которая изменяет счётчик.
На уровне языка можно контролировать правильность типов и допустимость операций с памятью.
Но для конкретной системы могут существовать дополнительные требования: счётчик должен изменяться строго на заданную величину, другое состояние не должно меняться, а при определённых условиях результат должен оставаться в установленном диапазоне.
Такие свойства уже являются требованиями самой системы.
В Sekura JS их можно описать отдельным формальным условием и проверить относительно скомпилированного машинного кода.
Поэтому формальная проверка интересуется не только вопросом «безопасна ли конструкция языка», но и вопросом «реализует ли программа требуемое поведение».
Почему Sekura JS не является заменой Rust
Rust — зрелый язык общего системного назначения с развитой экосистемой и поддержкой множества платформ. Он подходит для широкого круга задач, где необходимы производительность, системный контроль и защита от многих ошибок работы с памятью.
Sekura JS имеет существенно более узкую область.
Он развивается вместе с Memora8, Reganta и средствами формальной проверки Sekura. Его устройство определяется задачами этого программно-аппаратного стека.
Поэтому цель проекта не состоит в том, чтобы предложить альтернативу Rust для всех существующих системных программ.
Два разных пути к надёжности
Различие между Rust и Sekura JS хорошо показывает, что слово «надёжность» может означать разные вещи.
Один путь — сделать язык таким, чтобы он ещё при компиляции не позволял использовать многие опасные конструкции.
Другой путь — дать возможность явно сформулировать требуемое свойство и проверить, что конкретный машинный код действительно ему соответствует.
На практике эти идеи не противоречат друг другу. Строгие правила языка и формальные доказательства могут дополнять друг друга.
Для Sekura JS основным направлением сейчас является второе: связать исходную программу, результат компиляции и формальное требование так, чтобы свойства машинного кода можно было проверять воспроизводимым способом.
Именно поэтому сравнение с Rust для нас интересно не как соревнование двух языков, а как сравнение двух разных способов повышать доверие к системному программному обеспечению.
Share
