The post has been translated automatically. Original language: Russian
After the publication of materials about Sekura JS, one of the most frequent questions turned out to be simple: what problem does this language solve at all?
Sekura JS is not created because the world lacks another programming language. His task is related to another problem — how to build a software system in which you can consistently check the properties of not only a single function or algorithm, but also the entire chain from the processor to the application module.
The problem doesn't end with the program
Let's say we wrote a small program and formally proved that it works correctly under the given conditions. This is a useful result in itself, but the program does not exist separately from the surrounding system.
It runs on a processor, uses system software, memory, function call rules, and other platform mechanisms. If the proof concerns only the original algorithm, most of this chain remains outside of it.
For regular software, this is often acceptable. But for systems where increased reliability is required, a more difficult task arises: to understand which properties are confirmed at each level and on what assumptions the final statement about the system is based.
This is exactly the problem we want to solve in the Sekura stack.
From the processor to the application module
The goal of the project is to gradually build a complete vertical stack.:
Memora8 → Reganta OS → Sekura JS → software module
RTL Memora8 and formal verification via SJV are used for the hardware. For the software part, Sekura JS is compiled into a SOBJ machine object, the behavior of which SJV can check with respect to the semantics of Memora8 commands, a specified contract, and execution conditions.
Thus, Sekura JS occupies an intermediate place between the processor architecture and the system or application code. It is designed taking into account the fact that the compilation result must be sufficiently unambiguous for subsequent formal verification.
This is the main reason for the existence of the language.
Why did this require a separate language?
Sekura JS is a system language with an explicit memory model, a simple sample system, and a direct link to the Memora8 architecture.
He does not try to hide the machine's structure behind a large execution environment. On the contrary, the location of data, pointers, bit depth, function call rules, and other properties that affect the actual behavior of the program remain visible in the language.
For an ordinary application language, such restrictions might look superfluous. But for formal verification, predictability is more important than the number of language features.
The less hidden behavior there is between the source program and the machine code, the easier it is to determine exactly what is being tested.
It is not the source text itself that is being checked
In the current Sekura JS chain, the .sjs source file is compiled into several artifacts, including the .sobj executable.
SJV specifically checks the behavior of SOBJ's machine code with respect to the semantics of Memora8, the contract, and the explicitly defined environment. This is fundamental: the proof refers not just to the expression in the source text, but to the code that must be executed on the processor.
For example, a contract can specify acceptable initial states and the required state after the function is executed. Symbolic values do not represent one selected test case, but all values that meet the specified conditions.
If the requirement is violated, the examiner can obtain a counterexample. If a violation within the model is not possible, the result is recorded as a confirmed property for the specified verification area.
Why do we need the entire stack?
You can formally check a separate software module and leave it at that. But then some of the trust is transferred to other levels of the system anyway.
At Sekura, we want to reduce this area of assumptions gradually.
The Memora8 hardware is tested through a limited subset of SystemVerilog and SJV. The Sekura JS program code is validated through SOBJ and the ISA Memora8 model. Reganta OS should become the system layer between them.
As a result, it becomes possible to build not one big statement "the system is proven", but a chain of specific verifiable statements, for each of which the initial data, conditions and boundaries are known.
This is much more important than the name of the language itself.
What can it do?
This approach is needed primarily where routine testing alone is not enough and it is necessary to explain why the system should behave in a certain way.
We can talk about fault-tolerant systems, embedded equipment, industrial management, and other tasks where an error in one low-level component can affect the entire system.
Formal verification does not cancel testing. It answers another question: is it possible to confirm a specific property for the entire specified range of states, and not just for a set of completed tests.
This is still the way to go, not a statement about a fully proven system.
Today, some parts of this chain are already in operation.
For Sekura JS, there is a path from SJS through compilation in SOBJ to checking SJV and forming SJP. SJV is also being developed as an RTL Memora8 checker on SystemVerilog.
But this does not mean that the entire stack from the processor to the operating system and the application has already been formally proven.
On the contrary, one of the tasks of the project is to explicitly separate what has already been verified, what has only been modeled, which assumptions are used and which parts still need to be proved.
That is why we consider Sekura JS not as an independent new language for the sake of language, but as one of the elements of a broader system.
Its task is to make the software layer part of a formally verifiable end—to-end stack, where the properties of the system can be traced from the hardware to the executed software module.
После публикации материалов о Sekura JS один из самых частых вопросов оказался простым: какую проблему вообще решает этот язык?
Sekura JS создаётся не потому, что миру не хватает ещё одного языка программирования. Его задача связана с другой проблемой — как построить программную систему, в которой можно последовательно проверять свойства не только отдельной функции или алгоритма, но и всей цепочки от процессора до прикладного модуля.
Проблема не заканчивается на программе
Допустим, мы написали небольшую программу и формально доказали, что при заданных условиях она работает правильно. Само по себе это уже полезный результат, но программа не существует отдельно от окружающей системы.
Она исполняется на процессоре, использует системное программное обеспечение, память, правила вызова функций и другие механизмы платформы. Если доказательство касается только исходного алгоритма, большая часть этой цепочки остаётся за его пределами.
Для обычного программного обеспечения это часто приемлемо. Но для систем, где требуется повышенная надёжность, возникает более сложная задача: понять, какие свойства подтверждены на каждом уровне и на каких предположениях строится итоговое утверждение о системе.
Именно эту проблему мы хотим решать в стеке Sekura.
От процессора до прикладного модуля
Цель проекта — постепенно построить полный вертикальный стек:
Memora8 → Reganta OS → Sekura JS → программный модуль
Для аппаратной части используется RTL Memora8 и формальная проверка через SJV. Для программной части Sekura JS компилируется в машинный объект SOBJ, поведение которого SJV может проверять относительно семантики команд Memora8, заданного контракта и условий исполнения.
Таким образом, Sekura JS занимает промежуточное место между архитектурой процессора и системным или прикладным кодом. Он проектируется с учётом того, что результат компиляции должен быть достаточно однозначным для последующей формальной проверки.
Это и есть основная причина существования языка.
Почему для этого понадобился отдельный язык
Sekura JS — системный язык с явной моделью памяти, простой типовой системой и прямой связью с архитектурой Memora8.
Он не пытается скрыть устройство машины за большой средой исполнения. Напротив, в языке остаются видимыми расположение данных, указатели, разрядность значений, правила вызова функций и другие свойства, которые влияют на реальное поведение программы.
Для обычного прикладного языка такие ограничения могли бы выглядеть излишними. Но для формальной проверки предсказуемость важнее количества возможностей языка.
Чем меньше скрытого поведения между исходной программой и машинным кодом, тем проще точно определить, что именно проверяется.
Проверяется не исходный текст сам по себе
В текущей цепочке Sekura JS исходный файл .sjs компилируется в несколько артефактов, включая исполняемый объект .sobj.
SJV проверяет именно поведение машинного кода SOBJ относительно семантики Memora8, контракта и явно заданного окружения. Это принципиально: доказательство относится не просто к выражению в исходном тексте, а к тому коду, который должен выполняться на процессоре.
Например, контракт может задавать допустимые начальные состояния и требуемое состояние после выполнения функции. Символические значения представляют не один выбранный тестовый пример, а все значения, удовлетворяющие заданным условиям.
Если требование нарушается, проверяющий может получить контрпример. Если нарушение в пределах модели невозможно, результат фиксируется как подтверждённое свойство для заданной области проверки.
Зачем нужен весь стек
Можно формально проверить отдельный программный модуль и на этом остановиться. Но тогда часть доверия всё равно переносится на остальные уровни системы.
В Sekura мы хотим уменьшать эту область предположений постепенно.
Аппаратная часть Memora8 проверяется через ограниченное подмножество SystemVerilog и SJV. Программный код Sekura JS проверяется через SOBJ и модель ISA Memora8. Reganta OS должна стать системным слоем между ними.
В результате появляется возможность строить не одно большое утверждение «система доказана», а цепочку конкретных проверяемых утверждений, для каждого из которых известны исходные данные, условия и границы.
Это гораздо важнее самого названия языка.
Что это может дать
Такой подход нужен прежде всего там, где одного обычного тестирования недостаточно и необходимо объяснить, почему система должна вести себя определённым образом.
Речь может идти об отказоустойчивых системах, встроенном оборудовании, промышленном управлении и других задачах, где ошибка одного низкоуровневого компонента способна повлиять на всю систему.
Формальная проверка при этом не отменяет тестирование. Она отвечает на другой вопрос: можно ли подтвердить конкретное свойство для всей заданной области состояний, а не только для набора выполненных тестов.
Это пока путь, а не заявление о полностью доказанной системе
Сегодня отдельные части этой цепочки уже работают.
Для Sekura JS существует путь от SJS через компиляцию в SOBJ до проверки SJV и формирования SJP. SJV также развивается как средство проверки RTL Memora8 на SystemVerilog.
Но это ещё не означает, что весь стек от процессора до операционной системы и приложения уже формально доказан.
Напротив, одна из задач проекта — явно разделять, что уже проверено, что только смоделировано, какие предположения используются и какие части ещё требуют доказательства.
Именно поэтому мы рассматриваем Sekura JS не как самостоятельный новый язык ради языка, а как один из элементов более широкой системы.
Его задача — сделать программный слой частью сквозного формально проверяемого стека, где свойства системы можно прослеживать от аппаратуры до выполняемого программного модуля.
Share
