| |||||||||||||
Google's Native ClientGoogle's Native ClientPosted 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 http://www.springerlink.com/content/fw2u6488576w68j4/
(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.
|
|||||||||||||