Re: Verified OS concerns

2013-09-25 Thread iki tornsen 
Things change, computer dev evolves too
openbsd dev team uses audit code with great success
but many industrial domains uses new technics like static analysis  with
success too
for exemple in avionics soft : astrée is a tool that certified Airbus plane
software with static analysis
read astree web page 

in such domain perfection could not exist : church gödel turing in 1930 ...

but
it could be interesting for the core team to have a static analysis tool
to test OpenBSD kernel code
it will not be a simple task for sure but it's for my own opinion  a
necessity
 and keep openBSD far beyond ...

some researchers still have this in mind  ...  openbsd
superlint

in short and private joke : openbsd, (model) checks your 6 ! ... (release)
;)
Iki

Re: Verified OS concerns

2013-09-20 Thread Eric Johnson 
On Thu, 19 Sep 2013, josef.win...@email.de wrote:

> Does OpenBSD plan to varify its (main) components, to reach the level of 
> zero-bug software?

Just out of curiousity, how much verifying would it take to reach the 
level of "zero-bug software"? 

How would that affect the development cycle?

> If not, isn't there any concern that (future) varified OS will render 
> OBSD redundant one day?

Don't you think it will be a very, very, very long time before any 
operating system has zero bugs?  As it stands now, I suspect that OpenBSD 
is probably far ahead of most because the developers have spent a great 
deal of effort into reviewing the code for security concerns.

Eric

Re: Verified OS concerns

2013-09-20 Thread Eric Johnson 
On Thu, 19 Sep 2013, Peter N. M. Hansteen wrote:

> I remain unconvinced that it's possible to formally verify non-trivial
> code to be bug free. You remain free to convince me otherwise or point
> me to available verified non-trivial software roughly on par with a
> complete operating system.

Precisely.  

I would think that the effort to make sure that any major process is bug 
free would be tremendous.

Or you could do like I did once.  I wrote a system years ago on a VAX for 
processing and tracking traffic tickets that was on-time and worked really 
well.  The first bug that was discovered turned out to be rather useful 
and so I left it alone and it became a feature.

Unfortunately, that's the only bug I can think of in any of my code that 
was actually useful.

Eric

Re: Verified OS concerns

2013-09-19 Thread Bernte 

On 9/19/13 9:29 PM, josef.win...@email.de wrote:

Does OpenBSD plan to varify its (main) components, to
reach the level of zero-bug software?


I do assume that you are talking about "formal verification" meaning 
"mathematical proof of correctness".


Verify against what? Verification is a binary mathematical relation 
between a formal specification and an implementation. So, to start you 
need a specification. I have never seen a specification of a UNIX-like 
operating system that can claim completeness is any way. And if there 
was, it may contain as many bugs as the code. This is a dead end ...


Instead what you normally do is formally verifying certain, small 
aspects, like "are all variable initialized" or "will I ever be able 
access unallocated parts of the memory". Interestingly enough, whenever 
such a formal verification becomes practical, it is call "static 
checking" and then put into a tool like lint or valgrind.


Then, on the other hand, mindless use of such static checking itself can 
lead to severe bugs [1].



If not, isn't there any concern that (future) varified OS
will render OBSD redundant one day?


No.

Bernd

[1] http://research.swtch.com/openssl

Re: Verified OS concerns

2013-09-19 Thread Peter N. M. Hansteen 
pe...@bsdly.net (Peter N. M. Hansteen) writes:

> systems that have developed in response to real-world needs and formal
> standards specifications that at least in some cases more likely than
> not were in any way verified even to be internally consistent. 

missing a 'never' in there. clearer?

-- 
Peter N. M. Hansteen, member of the first RFC 1149 implementation team
http://bsdly.blogspot.com/ http://www.bsdly.net/ http://www.nuug.no/
"Remember to set the evil bit on all malicious network traffic"
delilah spamd[29949]: 85.152.224.147: disconnected after 42673 seconds.

Re: Verified OS concerns

2013-09-19 Thread Peter N. M. Hansteen 
josef.win...@email.de writes:

> Right, a varified full flaged OS is still future. 
> But there is nevertheless progress and affort.

Thanks for the pointeres, but anytime this comes up, an old AI
witticism turns up at the back of my head, 

  "If our mind were so simple we could actually understand it
   fully, we almost certainly couldn't be bothered to try"

(original source lost or not within reach of my puny attempts at web
search). The point is, formal verification is *hard*, and any flaws in
your formal verification procedure will put you back at essentially
square one, every time. Which will happen a lot when exposed to
systems that have developed in response to real-world needs and formal
standards specifications that at least in some cases more likely than
not were in any way verified even to be internally consistent. 

My money is still on the OpenBSD-style source code audits (aka
'reading the code like the devil reads the bible' for real-world
results.

- P
-- 
Peter N. M. Hansteen, member of the first RFC 1149 implementation team
http://bsdly.blogspot.com/ http://www.bsdly.net/ http://www.nuug.no/
"Remember to set the evil bit on all malicious network traffic"
delilah spamd[29949]: 85.152.224.147: disconnected after 42673 seconds.

Re: Verified OS concerns

2013-09-19 Thread Artturi Alm 

On 09/20/13 00:00, thornton.rich...@gmail.com wrote:

Interesting thread...
Sent from my BlackBerry 10 smartphone on the Verizon Wireless 4G LTE
network.



this is misc@, not twitter.
while i finally reply to message by you, i want to ask a question.
how about dropping at least the 'Wireless' out of your annoying
signature? it would fit in a single line.
I've never heard of Wired 4G LTE network.



> From: josef.winger@email.deSent: Thursday, September 19, 2013 4:30 PMTo:
> misc@openbsd.orgSubject: Verified OS concerns
>
> Does OpenBSD plan to varify its (main) components, to
> reach the level of zero-bug software?
>
> If not, isn't there any concern that (future) varified OS
> will render OBSD redundant one day?
>
> /jo
>

With the hardware at large, you're likely a troll for asking.

-Artturi

Re: Verified OS concerns

2013-09-19 Thread Nick Holland 

On 09/19/2013 04:29 PM, josef.win...@email.de wrote:

Does OpenBSD plan to varify its (main) components, to
reach the level of zero-bug software?


you mean, painfully reviewing and auditing code?
what do you think they've been trying to do for the last 15 years?
And after that, they have been trying to make sure when there are bugs 
anyway, they can't be exploited.  Over-all, they've been pretty darned 
successful.  Certainly more so than the people who have claimed to have 
a way to write perfect code.



If not, isn't there any concern that (future) varified OS
will render OBSD redundant one day?


I suspect few openbsd developers will ever be caught sitting around 
saying, "I'm bored".


You mean some mathamagical way to PROVE perfection?
don't hold your breath.
Don't get me wrong, I'd love to see a general purpose OS with the basic 
reliability of my car, and the ability to do ANYTHING with it without 
worrying about the security implications.  It would be fun to not worry 
about security.


But ... ain't gonna happen.
Been in this crap for 31 years now.  All the technology that's been 
thrown at the problem of security hasn't changed a thing.  We don't want 
to train users, so nothing is going to change.  We like features and 
performance over quality, so again, nothing is going to change.


At this point, it is your turn.  Shut up and produce your proven perfect 
OS, and show us the result.  Don't tell us it's possible, DO IT.  It's 
that simple.  Use any tools you want, write some non-trivial apps that 
make it useful for something.  I'll even spot you an eight core 2G RAM 
system to do what I was doing with 32M RAM and a 486 15 years ago.  When 
you have it, publish the source code and let us know.  I'll be the guy 
running the pool for when someone first pops it.  My $1 is on "five 
hours".  I hope I lose.


Nick.

Re: Verified OS concerns

2013-09-19 Thread Ted Unangst 
On Thu, Sep 19, 2013 at 22:29, josef.win...@email.de wrote:
> Does OpenBSD plan to varify its (main) components, to
> reach the level of zero-bug software?
> 
> If not, isn't there any concern that (future) varified OS
> will render OBSD redundant one day?

Short answer: no. Long answer: still no.

Re: Verified OS concerns

2013-09-19 Thread Kenneth R Westerback 
On Thu, Sep 19, 2013 at 10:29:39PM +0200, josef.win...@email.de wrote:
> Does OpenBSD plan to varify its (main) components, to
> reach the level of zero-bug software?

No. Zeno convinced us that you can't get there from here.

> 
> If not, isn't there any concern that (future) varified OS
> will render OBSD redundant one day?

No. Think of it as evolution in action.

 Ken

Re: Verified OS concerns

2013-09-19 Thread Marc Espie 
On Thu, Sep 19, 2013 at 05:14:37PM -0400, Nick Holland wrote:
> Don't get me wrong, I'd love to see a general purpose OS with the
> basic reliability of my car, 

Actually, it looks more and more like the reverse is coming true.

Re: Verified OS concerns

2013-09-19 Thread Peter N. M. Hansteen 
josef.win...@email.de writes:

> Does OpenBSD plan to varify its (main) components, to
> reach the level of zero-bug software?
>
> If not, isn't there any concern that (future) varified OS
> will render OBSD redundant one day?

I remain unconvinced that it's possible to formally verify non-trivial
code to be bug free. You remain free to convince me otherwise or point
me to available verified non-trivial software roughly on par with a
complete operating system.

Then again, I'm not a core OpenBSD developer, so you're free to ignore
me too.

And yes, September is like that isn't it?

- P

-- 
Peter N. M. Hansteen, member of the first RFC 1149 implementation team
http://bsdly.blogspot.com/ http://www.bsdly.net/ http://www.nuug.no/
"Remember to set the evil bit on all malicious network traffic"
delilah spamd[29949]: 85.152.224.147: disconnected after 42673 seconds.

Re: Verified OS concerns

2013-09-19 Thread thornton . richard 
Interesting thread...
Sent from my BlackBerry 10 smartphone on the Verizon Wireless 4G LTE
network.

From: josef.winger@email.deSent: Thursday, September 19, 2013 4:30 PMTo:
misc@openbsd.orgSubject: Verified OS concerns

Does OpenBSD plan to varify its (main) components, to
reach the level of zero-bug software?

If not, isn't there any concern that (future) varified OS
will render OBSD redundant one day?

/jo

Verified OS concerns

2013-09-19 Thread josef . winger 
Does OpenBSD plan to varify its (main) components, to
reach the level of zero-bug software?

If not, isn't there any concern that (future) varified OS
will render OBSD redundant one day?


/jo