User: Password:
Subscribe / Log in / New account

Google's Native Client

Google's Native Client

Posted Jun 4, 2009 7:52 UTC (Thu) by Thue (subscriber, #14277)
Parent article: Google's Native Client

even if all of the bugs with NaCl itself were found and fixed—an impossible task

A bit too categorically pessimistic, IMO. What if a formal proof was written that all programs which pass the validator are safe, and the formal proof itself was run through a proof validator?

That is not science fiction. Computer scientists are working on similar projects right now :). See for example

(Log in to post comments)

Google's Native Client

Posted Jun 4, 2009 14:03 UTC (Thu) by NAR (subscriber, #1313) [Link]

Scientists also work on power plant based on nuclear fusion :-) I think that will be ready earlier than an automatic prover.

Google's Native Client

Posted Jun 5, 2009 13:26 UTC (Fri) by Thue (subscriber, #14277) [Link]

Google already wrote the automatic prover. Now we just need to write the proof that the automatic prover is correct. Such a proof is written by hand with the current frontier science, and the proof is then checked by an automated proof validator.

I don't see anything here which is not already done today, just on a smaller scale.

Google's Native Client

Posted Jun 10, 2009 15:26 UTC (Wed) by amarjan (guest, #25108) [Link]

What about implementation defects -- say in a given stepping of a particular CPU?

I'm not a low lever programmer so I can't site relevant examples from memory, but I know there have been numerous such defects with security implications over the years.

Copyright © 2017, Eklektix, Inc.
Comments and public postings are copyrighted by their creators.
Linux is a registered trademark of Linus Torvalds