flat assembler
Message board for the users of flat assembler.

Index > Heap > 30 people-years to certify 7500 lines of code bug free

Goto page 1, 2  Next
Author
Thread Post new topic Reply to topic
revolution
When all else fails, read the source


Joined: 24 Aug 2004
Posts: 17271
Location: In your JS exploiting you and your system
revolution
http://www.unsw.edu.au/news/pad/articles/2009/sep/microkernel_breakthrough.html

Quote:
"A rule of thumb is that reasonably engineered software has about 10 bugs per thousand lines of code, with really high quality software you can get that down to maybe one or three bugs per thousand lines of code," Professor Heiser said.

"That can mean there are a lot of bugs in a system. What we’ve shown is that it’s possible to make the lowest level, the most critical, and in a way the most dangerous part of the system provably fault free."
Is it really possible to have large code bases bug free? Seems kind of suspect to me. Unless the kernel does almost nothing and is thus easier to test all the possible scenarios. Hmm ... Neutral
Post 25 Sep 2009, 15:19
View user's profile Send private message Visit poster's website Reply with quote
Borsuc



Joined: 29 Dec 2005
Posts: 2466
Location: Bucharest, Romania
Borsuc
Depends what you mean by "bug". Is it just software errors, or "cases I haven't thought of when programming it". The latter, I would call, just lack of features in all cases.
Post 25 Sep 2009, 16:22
View user's profile Send private message Reply with quote
LocoDelAssembly
Your code has a bug


Joined: 06 May 2005
Posts: 4633
Location: Argentina
LocoDelAssembly
Post 25 Sep 2009, 18:28
View user's profile Send private message Reply with quote
bitshifter



Joined: 04 Dec 2007
Posts: 764
Location: Massachusetts, USA
bitshifter
I like how they visualize function call paths with 3D graphics.
Now if i could only get that picture to rotate on its 3 axis...
Post 25 Sep 2009, 18:45
View user's profile Send private message Reply with quote
ManOfSteel



Joined: 02 Feb 2005
Posts: 1154
ManOfSteel
No code can ever be 100% bug free, especially if it's frequently updated as is the case with any OS/program in the REAL world, even those specifically made for "advanced uses".

Maybe it's only possible with a lab rat microkernel written in less than 10,000 lines of code and rarely (if ever) updated.

Is such a lengthy verification feasible in terms of financial costs, and human and technical resources requirements? Is it even possible in temporal terms for anything longer than 7,500 lines of C code? What about a 100,000 lines "non-micro"-kernel? What about +1,000,000 lines for a complete system?



Borsuc wrote:
Is it just software errors, or "cases I haven't thought of when programming it". The latter, I would call, just lack of features in all cases.

But this would be too easy, and reality is more complicated than that.

A lot of critical security vulnerabilities are not caused by "badly written" code (i.e. a programming error in one specific line) at all, but by other lines that are missing... because the programmer didn't think of it when programming.
These vulnerabilities, for instance, may be caused by checks for certain conditions that have not been implemented, and are thus exploited by attackers. This is more or less what they have been checking for all eternity (cf. What the proof implies).

This is very different from a program that lacks, say, a -v parameter for verbose mode.
Post 25 Sep 2009, 21:27
View user's profile Send private message Reply with quote
rCX



Joined: 29 Jul 2007
Posts: 166
Location: Maryland, USA
rCX
ManOfSteel wrote:
No code can ever be 100% bug free,


A simple hello world program, written in asm, can be completely bug free Razz You would really have to suck at coding to mess it up. I also imagine that many of the 256 byte demos are flawless.
Post 25 Sep 2009, 22:41
View user's profile Send private message Reply with quote
sleepsleep



Joined: 05 Oct 2006
Posts: 8885
Location: ˛                             ⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣Posts: 334455
sleepsleep
why not everybody use the l4 verified kernel? Instead of other unverified bloat?
And i felt if the design start from very conscious and carefull step,it wouldnt produce any noticeable bugs.
but is there any verified bug free kernel for x86 system?
Even linus said linux kernel is bloat,so i guess no much hope for us to rely on it.
Why not they scrap everthing and start again,i think that would be easier for long term.
Post 25 Sep 2009, 22:58
View user's profile Send private message Reply with quote
bitshifter



Joined: 04 Dec 2007
Posts: 764
Location: Massachusetts, USA
bitshifter
They would rather make money rather than the perfect OS.
Post 25 Sep 2009, 23:27
View user's profile Send private message Reply with quote
revolution
When all else fails, read the source


Joined: 24 Aug 2004
Posts: 17271
Location: In your JS exploiting you and your system
revolution
Thanks for the better link LocoDelAssembly.

It is a pity they have not even bothered to attempt to certify the ARM assembly parts. They just ignored it and put it as an assumption of correctness to achieve the bug free status. So in reality they still have a weak link with all the extra code that they use but don't certify. I cannot find any reference to suggest that they are going to complete the tests and certify it in the future. Does that mean assembly code is just too hard to get right? Or maybe just too hard to verify that it is right? Both?
Post 26 Sep 2009, 07:27
View user's profile Send private message Visit poster's website Reply with quote
Madis731



Joined: 25 Sep 2003
Posts: 2141
Location: Estonia
Madis731
I have dreamed my whole life about THIS: http://ertos.nicta.com.au/research/drivers/synthesis/home.pml

This article is full on pure insanity Very Happy http://ertos.nicta.com.au/publications/papers/Ryzhyk_CKSH_09.pdf (I mean it in a good way).
Post 26 Sep 2009, 09:50
View user's profile Send private message Visit poster's website Yahoo Messenger MSN Messenger Reply with quote
ManOfSteel



Joined: 02 Feb 2005
Posts: 1154
ManOfSteel
rCX wrote:
I also imagine that many of the 256 byte demos are flawless.

This is not certified. And most are visual demos, nothing more. Only few of them are useful in the real world (attrib, ls/dir, etc).
Also, we're talking here about much more elaborate programs and OS kernels that *require* several thousand lines of code for their basic function.
Post 26 Sep 2009, 10:20
View user's profile Send private message Reply with quote
ManOfSteel



Joined: 02 Feb 2005
Posts: 1154
ManOfSteel
sleepsleep wrote:
why not everybody use the l4 verified kernel?

Maybe because it's useless by itself.
It's also impractical. It takes too much time, people, money, etc. to be used in the real world. What happens when they update it and modify or add 1,000 lines? They have to re-allocate all these resources to verify the *whole* code again. I said "whole", because it's not enough to check the new code only but also be sure that it doesn't break the functionality of the old code and that the interaction with it works flawlessly.
Besides the L4 is just a micro-kernel. You know what it means, right? What about all the rest? Can they still efficiently verify and certify as clean the hundred thousands more lines in the userland (including device drivers)?

sleepsleep wrote:
Instead of other unverified bloat?
And i felt if the design start from very conscious and carefull step,it wouldnt produce any noticeable bugs.

Easier said than done. Competent OS developers spend hours and days checking every line of their code. In some projects, it's checked again by other teams of security specialists. If it's OSS, it may even be checked again by thousands of people around the world and by security experts. But some bugs always slip through and are only discovered years later. And you know why? Because all these people are humans, and to err is human.

sleepsleep wrote:
but is there any verified bug free kernel for x86 system?

I'm already skeptic about the L4 kernel itself. And unless someone proves me wrong by taking an existing non-micro-kernel with more than 7,500 lines of code (or a micro-kernel with its entire userland system source) and certifying it as totally clean, I'll remain convinced it's just impossible to do it in the real world. And even then, no one can be *100%* sure. What if a bug is discovered 50 years later? No one will still be alive to tell them they missed it and were wrong.

sleepsleep wrote:
Even linus said linux kernel is bloat

Yeah, let's all make micro-kernels! All "useless" code off kernel space! Let's all throw away 20-30 years of hard work and start with a clean slate.
BTW, there are cleaner kernels than Linux, even modular monolithic ones.

sleepsleep wrote:
so i guess no much hope for us to rely on it

Humm, it may not be better than the mostly useless lab rat L4 kernel, but at least it's a *little* better than other kernels I won't name.
Post 26 Sep 2009, 10:51
View user's profile Send private message Reply with quote
ManOfSteel



Joined: 02 Feb 2005
Posts: 1154
ManOfSteel
revolution wrote:
Does that mean assembly code is just too hard to get right? Or maybe just too hard to verify that it is right? Both?

Or too good and obviously bug free to be verified! Razz
Post 26 Sep 2009, 11:04
View user's profile Send private message Reply with quote
sleepsleep



Joined: 05 Oct 2006
Posts: 8885
Location: ˛                             ⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣⁣Posts: 334455
sleepsleep
Quote:

BTW, there are cleaner kernels than Linux, even modular monolithic ones.

hmm, example? in x86 architecture?
Post 26 Sep 2009, 11:49
View user's profile Send private message Reply with quote
ManOfSteel



Joined: 02 Feb 2005
Posts: 1154
ManOfSteel
*BSD.
Post 26 Sep 2009, 11:55
View user's profile Send private message Reply with quote
LocoDelAssembly
Your code has a bug


Joined: 06 May 2005
Posts: 4633
Location: Argentina
LocoDelAssembly
revolution, in some part it says this:
Quote:
These specific assumptions are not a limitation of the general formal verification approach. In theory, it is possible to eliminate all of them: there are successful verification projects showing the correctness of even optimising C compilers; there are at least two prominent research groups that have demonstrated successful formal verification of assembly code and low-level hardware management functions; we have ourselves proved an earlier version of the boot code correct down to the level of a precise, executable specification; and we have a separate formalisation of ARM11 virtual memory from first principles. There are still significant scientific challenges in unifying all of these into a single framework, but it is clear at this point that it can be done.
Post 26 Sep 2009, 14:56
View user's profile Send private message Reply with quote
bitshifter



Joined: 04 Dec 2007
Posts: 764
Location: Massachusetts, USA
bitshifter
But what if the bug checking routines have bugs?
Maybe these routines would lie and say there are no bugs...
Seems like a lot of work when you can just do it right once.
Post 26 Sep 2009, 20:04
View user's profile Send private message Reply with quote
ManOfSteel



Joined: 02 Feb 2005
Posts: 1154
ManOfSteel
bitshifter wrote:
But what if the bug checking routines have bugs?
Maybe these routines would lie and say there are no bugs...
Seems like a lot of work when you can just do it right once.

Near the end of this page, there are Q/A about this. I wasn't very convinced...
Post 26 Sep 2009, 21:51
View user's profile Send private message Reply with quote
Madis731



Joined: 25 Sep 2003
Posts: 2141
Location: Estonia
Madis731
Guys - please don't make this very practical project a discussion on philosophy! What they did is great. Software can have bugs, but they eliminated them using mathematical proof. There is no bug-checking done as we are use to, they incrementally grow the code.

Actually when you have proved some of the code, with the introduction of new code, you don't have to check it all. You only need to check the new code against the existing one, but only the portion, which it interacts with.

Maybe sometimes you need to throw away 20 years of development. Think SSD because it has little to do with magnetic discs. You can't reuse much of the knowledge. Think multiple cores and how differently they behave. Old kernels were all built with a single CPU in mind.

I applaud this approach although I admit that it is a very tedious task, but I think its worth it. Internet wouldn't be the same if it weren't for the ".com bubble" {I watch Discovery}. I think we will be coding in Termite in the near 20 years or so.
Post 26 Sep 2009, 21:56
View user's profile Send private message Visit poster's website Yahoo Messenger MSN Messenger Reply with quote
revolution
When all else fails, read the source


Joined: 24 Aug 2004
Posts: 17271
Location: In your JS exploiting you and your system
revolution
LocoDelAssembly wrote:
revolution, in some part it says this:
Quote:
These specific assumptions are not a limitation of the general formal verification approach. In theory, it is possible to eliminate all of them: there are successful verification projects showing the correctness of even optimising C compilers; there are at least two prominent research groups that have demonstrated successful formal verification of assembly code and low-level hardware management functions; we have ourselves proved an earlier version of the boot code correct down to the level of a precise, executable specification; and we have a separate formalisation of ARM11 virtual memory from first principles. There are still significant scientific challenges in unifying all of these into a single framework, but it is clear at this point that it can be done.
I've been trying to find the verification details for that ASM proof. But it does not apply to the code used in the seL4 download. I had kind of hoped that something like this might help me when coding, but from what I have seen so far it is very expensive and very time consuming. Hardly much good for a small company, let alone an individual. This is where the big guys with money and/or time have an advantage.

But I am curious to learn what were the 144 bugs found by the verifier. It might shed some light upon what sort of mistakes humans can easily miss.
Post 27 Sep 2009, 09:09
View user's profile Send private message Visit poster's website Reply with quote
Display posts from previous:
Post new topic Reply to topic

Jump to:  
Goto page 1, 2  Next

< Last Thread | Next Thread >
Forum Rules:
You cannot post new topics in this forum
You cannot reply to topics in this forum
You cannot edit your posts in this forum
You cannot delete your posts in this forum
You cannot vote in polls in this forum
You can attach files in this forum
You can download files in this forum


Copyright © 1999-2020, Tomasz Grysztar.

Powered by rwasa.