OpenBSD code and mathematical proofs

[psypro]

OpenBSD and proven secure

"I want to point out that "provably secure" has a specific definition which refers to formal verification through the use of mathematical proofs" https://www.quora.com/Can-computer-p...rovably-secure

a) Should OpenBSD base program take aim to be written in such a manner that they can be mathematically proven, like seL4?

b) If so is C the language for the further for OpenBSD, or are more complex compilers/languages like Rust needed to improve code correction to a level where it can be mathematically somewhat proven?

I am no dev. Just want to learn.

[e1-531g]

Formal verification is a very time consuming process. Designing something that can be formally verified is very consuming process. seL4 is just few thousand lines of code, so it can be designed (microkernel) and formally verified. Something the size of OpenBSD kernel with all the drivers is beyond resources such as work hours.
Even then formal verification it does not tells you that you can be sure this system is secure. It only proves that code is doing everything that is written in description of code. If assumptions of description are incomplete or wrong, the code probably have bugs.
Of course formal verification improves code quality by orders by magnitude.

You also should keep in mind that world changes. Hardware changes. Protocols are changing. Your project must be flexible enough to adapt to this changes and incorporate new features at reasonable pace.

https://theinvisiblethings.blogspot....rnels-and.html

[jggimi]

Consider the size of the "proof" that would be required. seL4 is a micro kernel. Just a kernel, consisting of 1100 files, with 95,000 lines of code.

OpenBSD is a complete operating system. That system consists of:

• A monolith kernel with more than 500 integrated drivers. The kernel alone is more than 7000 program files and contains nearly 3 million lines of code.
• The userland consts of approximately 3000 separate executables and libraries, consisting of nearly 70,000 program files and contains more than 21.5 million lines of code.

Good luck!


Sources:
OpenBSD -current /usr/src, find(1), xargs(1), wc(1), grep(1), and editors/libreoffice.
SeL4 project source at github: project seL4/seL4

[e1-531g]

Originally Posted by jggimi

Consider the size of the "proof" that would be required. seL4 is a micro kernel. Just a kernel, consisting of 1100 files, with 95,000 lines of code.

Paper from around 2009 states that:
http://web1.cs.columbia.edu/~junfeng...apers/sel4.pdf

seL4, a third-generation microkernel of L4 prove-
nance, comprises 8,700 lines of C code and 600 lines
of assembler.

and assembly code actually was not formally verified.

Generally speaking general purpose operating systems are not bug free. However I think that it would be possible that some small parts of it can be formally verified. There is a concept of privilege separation. It is implemented in OpenSSH daemon and Chromium. There is small, trusted part of program and a few other parts which are untrusted and large. It would be very interesting if somebody could write formally verified small, trusted part of these projects. It would be interesting if somebody could write formally verified pledge kernel's subsystem.

[jggimi]

Originally Posted by e1-531g

Paper from around 2009 states...

I used the 2017 kernel source repository on Github for the numbers I posted above.

[gpatrick]

Consider the size of the "proof" that would be required. seL4 is a micro kernel. Just a kernel, consisting of 1100 files, with 95,000 lines of code.

OpenBSD is a complete operating system. That system consists of:

Plan 9 is a complete operating system and the kernel is only 150,000+ lines of code. Add in a few thousand more for libs, userland and such, but it is still rather small.

[psypro]

"It would be very interesting if somebody could write formally verified small, trusted part of these projects. It would be interesting if somebody could write formally verified pledge kernel's subsystem. "

I agree, but I am open to being wrong.

I think if OpenBSD dev community managed to write some small part of OpenBSD in a mathematically proven way, they would learn something while doing it, that would in the long therm improve code quality of the rest of the project as well.

Because the development infrastructure regarding compilers/programming languages probably would need to be improved in order to do such task. C is only practically possible to prove in very small code, from my understanding after googling.

[jggimi]

psypro, we aren't project members here. We're users, just like you. This website is not affiliated with the OpenBSD project.

I expect that if you posted your suggestion on an official project channel, such as the misc@ mailing list -- the project would reject your suggestion. In my experience, the project does not accept development suggestions from the community at all. It has limited resources and expends them as they see fit, on areas of interest to its members.

However, development work by users and third parties is welcome. Submitted patches may be accepted, may be returned for further revision, or may be rejected. But they are reviewed.

So, if a non-project member -- you, for example -- were to conduct a "provably secure" analysis and submit your results along with your proposed source code changes to the tech@ mailing list, I am certain your proposed revisions would receive an assessment from the project.

[ocicat]

Originally Posted by psypro

"It would be very interesting if somebody could write formally verified small, trusted part of these projects. It would be interesting if somebody could write formally verified pledge kernel's subsystem. "

There is hardware simple enough to make it possible to thoroughly test all aspects. Software is exponentially more complicated -- complicated enough to make the process of testing every code path impossible

Yes, there have been people of late who talk that software is now mathematically provable, but I have yet to find a complete argument which proves this beyond doubt. I am still of the opinion that the problem is still so complicated that it is not worth a lot of discussion -- even for small portions of a kernel.

I think if OpenBSD dev community managed to write some small part of OpenBSD in a mathematically proven way, they would learn something while doing it, that would in the long therm improve code quality of the rest of the project as well.

Your argument implies that all details are known -- all bugs existing in the compilers or interpreters used as well as the processor itself. I can tell you from experience that hardware manufacturers don't make all bugs public. Trying to "prove" correctness cannot get around the politics and impracticality of trying to expose all details that manufacturers are not willing to air to the world.

If so is C the language for the further for OpenBSD, or are more complex compilers/languages like Rust needed to improve code correction to a level where it can be mathematically somewhat proven?

Again, the argument does not take into account the realities of implementation issues. Some compilers are better at translating higher level logic into processor instructions than other tools. So when others claim that they have mathematically proven the correctness of a particular chunk of software, do they say on what processor using a specific set of tools? If they don't, what is it that they are proving?

And when the tools change, are "they" going back & re-verifying that all translations used in the previous verification are still exactly the same with a newer toolchain? Proving correctness then becomes a never-ending process, and who is going to do this? And how fast can they do it? And are they testing on an ecosystem of hardware & software that resembles my hardware & software of choice?

I know there are those that claim that the abstractions implemented by languages such as Rust are "significantly better than C", but show me a perfect Rust compiler. There isn't one, just like there isn't a perfect C compiler. Making claims of "my memory model is better than your memory model" don't hold a lot of weight either because it all comes down to what is the implementation doing on a specific piece of hardware. If you dig into the history of OpenBSD's tools, you will find that there are a number of compiler fixes implemented by the project developers to the compilers used in the various OpenBSD platform supported. No other platform implements everything used here. And there is likely other projects which implement compiler fixes which are not universally shared everywhere, too.

So how does this fall into your argument of "mathematically proving" the OpenBSD system? Who is doing the proving on what platform using what toolchain? I don't ever see this level of detail stated in the underlying provability claims. If these details are not being aired openly, I question what it is that is being proven. Again, the fundamental problem is so complicated that many will say that their time is better spent doing other things. I tend to agree with them.

[e1-531g]

@ocicat
Mathematically proven software often have not one, but a several of them. Each proof is about one thing.
A lot of your doubts are addressed by seL4's FAQ.
https://wiki.sel4.systems/FrequentlyAskedQuestions
https://sel4.systems/Info/FAQ/proof.pml

Mathematically proven software competes with high-assurance software. Software is used not only by laptops, smartphones and servers. There are also microcontrollers found in cars, planes. Software found in them is more stable (or at least should be because life depends on it and it is doable) than OpenBSD, Gnu/Linux, Windows and any other general-purpose operating system by a few orders of magnitude. There are people who know how to do it.

Of course verification of all OpenBSD code is beyond Project resources and I doubt that even biggest IT corporations could do that.