Will the formal verification of a microkernel code allow creating super-reliable OS?

In 2015, the American company Rockwell Collins, together with Boeing and 3D-Robotics, conducted tests of the resistant to cracking quadrocopter Iris and unmanned helicopter Little Bird with an "ultra-reliable" operating system.

The development of burglar-protected drones is being commissioned by the Defense Advanced Agency Projects (DARPA) of the US Department of Defense, which is interested in protecting promising unmanned and optionally manned aircraft from possible vulnerabilities.

There are at least three ways to hack unmanned aerial vehicles: the first is to gain access to the management by hacking the communication channel or replacing authorization data, the second is using software vulnerabilities, the third is using interfaces and original software data channels to download malicious code.
')
The operating system based on the seL4 microkernel developed by Rockwell Collins is resistant to all three types of hacking. The operating system based on seL4 is initially focused primarily on security. In English, this is called a beautiful phrase "hackproof" (burglar resistant).

Its feature is a kernel resistant to code substitutions, which uses mathematical algorithms and checksums to check running services and also provides separate execution of processes.

The system allows you to start a virtual machine in which the guest program does not get access to the main processes or hardware. When the program is started, the checksums are reported to the kernel, on the basis of which errors are corrected or unauthorized processes are closed.

The tests were successful: cybersecurity experts could not run malicious code on unmanned vehicles with a protected operating system, and also take control of the drone or cause a system failure.


The seL4 microkernel is used not only in aviation, but also in medicine, the financial sector, energy, and other areas where a guarantee of non-failure is needed.

An important feature of the seL4 architecture is the removal of parts for managing kernel resources into user space and using the same access control for these resources as for user resources. The microkernel does not provide ready-made high-level abstractions for managing files, processes, network connections, and so on.

Instead, it provides only minimal mechanisms for controlling access to the physical address space, interrupts, and processor resources.

High-level abstractions and drivers for interacting with hardware are implemented separately - on top of the microkernel in the form of tasks performed at the user level. Access of such tasks to the resources of the microkernel is organized through the definition of rules.

For programmers, there is a component-oriented application development platform CAmkES , which allows to model and create systems based on seL4 as a collection of interacting components.

The L4.verified project, a formally verified core on the L4 architecture, is genetically related to seL4.

L4 is a second-generation microkernel developed by Jochen Liedtke in 1993.

The architecture of the L4 microkernel was successful. Many implementations of the ABI and API L4 microkernel have been created. All implementations came to be called the “L4 micronucleus family”. So seL4 appeared. And the Lidtke implementation was unofficially called “L4 / x86”.

The main idea of ​​L4.verified, like seL4, is to mathematically prove the correctness of the kernel implementation. The fact is that microkernels, in contrast to monolithic modular monsters like GNU / Linux, are very tiny in size. And if so, then they can be formally verified. Each line of code is matched with a mathematical statement that needs to be proved.

The L4.verified micronucleus proves compliance with the model implementation, the absence of perpetual loops, and some more things. The cost of this study was about $ 6 million, and the project lasted 7 years. The volume of work reached 25 man-years.

In addition to its main use (safety, as with seL4), L4 is used in other areas. So, Qualcomm has launched an implementation of the L4 microkernel developed by NICTA on a chipset called Mobile Station Modem ( MSM ). This was reported in November 2005 by representatives of the company NICTA, and in late 2006, MSM chipsets went on sale. So the implementation of the L4 microkernel was in cell phones.

The issue of creating highly reliable software became particularly relevant when the vast majority of applications began to work on the network and operate with large amounts of data. And these data are often confidential.

There are not so many materials on the network about the role of formal verification in creating super-reliable operating systems. Even less detailed discussions. Therefore, below we present the main thoughts and arguments of one of the conversations about the article on this topic:

• Distributing verification tools and correctly implementing them will get rid of a whole class of errors in any software. For example, such an error as “buffer overflow” can be prevented if it is enough to simply organize the verification of the required parameters.

There are still bugs there, one of the commentators concludes, referring to this material .

• The seL4 code is claimed to have some degree of reliability. If creating an OS that is completely protected from hacking is utopia, then why do such tough teams like DARPA continue to do this?

• What will happen if hackers slip the verified code there? Or is it impossible? Why are all the OS bugs that hackers can use?

• Why code verification must be associated with protection against hacking? What can not be easier? Code verification and protection against hacking are two different tasks that only sometimes overlap.
  
  Trojans, cyber rape, phishing, clickjacking are types of attacks that work regardless of the presence of errors in the program code of the application or the operating system as a whole. And if users choose weak passwords? Is it also the fault of software developers?

• The experiment is at odds with the reality, since the access that researchers gave to hackers in their lives no one will open. In such systems, you just need to carefully monitor in order to prohibit the insertion of code to everyone except the administrator.

• Wow! Well written and tested applications are very hard to crack. Who would have thought ... Actually, the program code consists of mathematically verified constructions.

• Developing a verified code is a luxury few can afford. And accompanying it and making constant changes is an even greater luxury.

• From a management perspective, programmers often behave bipolarly. When you ask them to break a big development task into subtasks, they easily agree. But when you offer them to think in advance about possible mistakes and systematically prevent them - the reaction is completely different: “it’s impractical”, “you don’t foresee everything”, “what about it?”, “How is it?” ... Not everyone wants to think about quality code in advance.

• And what if the verification tools themselves contain errors? Who will verify the verifiers?

• In pure math there are no “bugs”. If there is a rule that it is impossible to divide by zero, then the cases when zero is in the denominator are simply not considered. In real life, this technique does not work. If we are talking about software development, then we have to work there even with the meanings that the program doesn’t like. The result of dividing by zero is infinity. And it is necessary to do something with it, and not to declare that there can be no such result.

PS Of course, you can debate endlessly. But if such large organizations as DARPA take concrete steps to implement these projects, it is worth keeping a close eye on this story and at the very least take part.

The seL4 source code is still available on github .