[Cryptography] Has formal verification actually been useful in the real world?

[Bill Frantz]

On 3/11/17 at 6:41 AM, perry at piermont.com (Perry E. Metzger) wrote:

>On Sat, 11 Mar 2017 15:28:18 +1000 "James A. Donald"
><jamesd at echeque.com> wrote:
>>Has a complete formally verified system been deployed anywhere?
>
>...
>
>>Or a formally verified browser?
>
>There isn't one that has been deployed, but an experimental formally
>verified browser called Quark was built at UCSD. It hasn't been
>deployed and isn't maintained, but it was a very interesting
>demonstration because it showed how to use a small formally verified
>"software firewall" to contain millions of lines of very bad code that
>constituted the bulk of the browser.
>
>http://goto.ucsd.edu/quark/

Reporting in 2002, there was a DARPA funded project which 
resulted in "The DARPA Browser". Although not formally verified, 
it was designed to severely limit the privileges available to 
the renderer so a hostile renderer could not damage either the 
browser or the underlying system. The code and design were 
attacked by a tiger team. See: <http://www.combex.com/papers/darpa-report/html/>.

Cheers - Bill

-------------------------------------------------------------------------
Bill Frantz        | The first thing you need when  | Periwinkle
(408)356-8506      | using a perimeter defense is a | 16345 
Englewood Ave
www.pwpconsult.com | perimeter.                     | Los Gatos, 
CA 95032