Published on: 2026-09-01
Source: Novosibirsk State University –
An important disclaimer is at the bottom of this article.
On August 28, an event took place at Novosibirsk State University final conference of the Summer System Bootcamp, organized with the support of YADRO partner company. For two weeks, the students worked on projects in the field of systems development and low-level programming, and at the final meeting, they presented the results of their work.
Participants formed teams based on research interests and, under the guidance of mentors, tackled practical tasks. Among the projects were the development of an operating system in Rust, work on a reproducible compiler build chain on “bare metal”, deductive verification of a program, and performance research of a new processor with RISC-V architecture featuring specialized cores for neural network processing.
One of the projects was devoted to the problem of trust in the compiler build chain (the Reflecting Trust / Trusting Trust class of attack). Participants developed a trusted minimalist bootstrap toolchain, starting from a verifiable minimal-size source binary file. All subsequent build stages were deployed based on verifiable data formats and fixed artifacts. The team’s ultimate goal was to build the TCC (Tiny C Compiler), ensure complete determinism (repeatability) of the build process, and successfully run it on the target RISC-V architecture.
Another team worked on formal verification of an implementation of matrix multiplication. The participants used the Frama-C platform and dealt with code correctness conditions, including considerations related to memory operation characteristics.
– The need for deductive verification has been clear for decades. However, in practice, it is very complex. That is why deductive verification remained confined to scientific laboratories for a long time and struggled to penetrate practical applications. Only recently have automation methods emerged that make it possible to apply it to practical problems.
In this project, it was very important to understand whether students could master effective verification in a fairly short period of time and apply it to a real matrix multiplication implementation program. I consider it a very positive result of the project that the participants, with little prior preparation, studied such a complex subject in two weeks and at the same time successfully completed the verification of a real matrix multiplication program. – said the project curator Dmitry Kondratyev.
Project participant Alisa told that at the beginning of the bootcamp, her team faced the need to constantly revise the initial approach:
– I came with the task of comprehensive verification of matrix multiplication using one of the platforms we used—Frama-C. We were able to prove the effectiveness of this approach. We used assembler inserts, created correctness conditions for the code, proved them using Frama-C, and obtained the result.
The most difficult part was that for two weeks we constantly revised the idea: there were problems with Frama-C and with the fact that there are some memory limitations. Therefore, there were different options for how we could represent memory in the code and how to work with it. Some ideas did not work out; they were incorrect from a theoretical perspective, and in the end, we came to a fairly good solution.
The bootcamp concluded with participants receiving commemorative gifts from the company YADRO. For the teams, the intensive was an opportunity to try their hand in a new field, work on real practical tasks, and gain experience in collaborative development under the guidance of experts.
Please note; This information is raw content obtained directly from the information source. It represents an accurate report of what the source claims and does not necessarily reflect the position of MIL-OSI or its clients.