DaemonForums  

Go Back   DaemonForums > OpenBSD > OpenBSD General

OpenBSD General Other questions regarding OpenBSD which do not fit in any of the categories below.

Reply
 
Thread Tools Display Modes
  #1   (View Single Post)  
Old 10th January 2017
psypro psypro is offline
Shell Scout
 
Join Date: Mar 2016
Location: Continent:Europe
Posts: 124
Default OpenBSD code and mathematical proofs

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.
Reply With Quote
  #2   (View Single Post)  
Old 11th January 2017
e1-531g e1-531g is offline
VPN Cryptographer
 
Join Date: Mar 2014
Posts: 369
Default

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
__________________
Signature: Furthermore, I consider that systemd must be destroyed.
Based on Latin oratorical phrase
Reply With Quote
  #3   (View Single Post)  
Old 11th January 2017
jggimi's Avatar
jggimi jggimi is offline
More noise than signal
 
Join Date: May 2008
Location: USA
Posts: 5,944
Default

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

Last edited by jggimi; 11th January 2017 at 02:22 AM. Reason: typos
Reply With Quote
  #4   (View Single Post)  
Old 11th January 2017
e1-531g e1-531g is offline
VPN Cryptographer
 
Join Date: Mar 2014
Posts: 369
Default

Quote:
Originally Posted by jggimi View Post
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
Quote:
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.
__________________
Signature: Furthermore, I consider that systemd must be destroyed.
Based on Latin oratorical phrase
Reply With Quote
  #5   (View Single Post)  
Old 11th January 2017
jggimi's Avatar
jggimi jggimi is offline
More noise than signal
 
Join Date: May 2008
Location: USA
Posts: 5,944
Default

Quote:
Originally Posted by e1-531g View Post
Paper from around 2009 states...
I used the 2017 kernel source repository on Github for the numbers I posted above.
Reply With Quote
  #6   (View Single Post)  
Old 11th January 2017
gpatrick gpatrick is offline
Package Pilot
 
Join Date: Nov 2009
Posts: 208
Default

Quote:
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.
Reply With Quote
  #7   (View Single Post)  
Old 11th January 2017
psypro psypro is offline
Shell Scout
 
Join Date: Mar 2016
Location: Continent:Europe
Posts: 124
Default

"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.
Reply With Quote
  #8   (View Single Post)  
Old 11th January 2017
jggimi's Avatar
jggimi jggimi is offline
More noise than signal
 
Join Date: May 2008
Location: USA
Posts: 5,944
Default

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.

Last edited by jggimi; 11th January 2017 at 03:14 PM. Reason: typo
Reply With Quote
  #9   (View Single Post)  
Old 12th January 2017
ocicat ocicat is offline
Administrator
 
Join Date: Apr 2008
Posts: 3,276
Default

Quote:
Originally Posted by psypro View Post
"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.
Quote:
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.
Quote:
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.

Last edited by ocicat; 12th January 2017 at 06:27 AM. Reason: add clarity
Reply With Quote
Old 12th January 2017
e1-531g e1-531g is offline
VPN Cryptographer
 
Join Date: Mar 2014
Posts: 369
Default

@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.
__________________
Signature: Furthermore, I consider that systemd must be destroyed.
Based on Latin oratorical phrase

Last edited by e1-531g; 12th January 2017 at 09:37 AM.
Reply With Quote
Reply

Thread Tools
Display Modes

Posting Rules
You may not post new threads
You may not post replies
You may not post attachments
You may not edit your posts

BB code is On
Smilies are On
[IMG] code is On
HTML code is Off

Forum Jump

Similar Threads
Thread Thread Starter Forum Replies Last Post
Does OpenBSD use libarchive sandboxing code? betweendayandnight OpenBSD Security 4 13th August 2016 06:46 PM
Google Summer of Code - OpenBSD shep News 9 14th September 2014 07:44 PM
New Open DRM code for OpenBSD shep News 0 22nd March 2013 02:32 AM
*** Error code 1 building OpenBSD 5.1-stable from source comet--berkeley OpenBSD Installation and Upgrading 12 19th May 2012 02:18 AM
Compiling OpenBSD code WeakSauceIII OpenBSD General 4 19th May 2008 12:59 AM


All times are GMT. The time now is 02:02 AM.


Powered by vBulletin® Version 3.8.4
Copyright ©2000 - 2017, Jelsoft Enterprises Ltd.
Content copyright © 2007-2010, the authors
Daemon image copyright ©1988, Marshall Kirk McKusick