[Cryptography] Formal Verification

[Perry E. Metzger]

On Fri, 18 Mar 2016 09:32:07 +0800 Ilya Levin <ilevin at gmail.com>
wrote:
> On Fri, Mar 18, 2016 at 12:18 AM, Jonathan Thornburg <
> jthorn at astro.indiana.edu> wrote:  
> 
> > Indeed, it would seem to provide an interesting vehicle for
> > producing a formally-verified TCP/IP stack.  Has anyone tried
> > this? 
> 
> To do a DSL for producing a formally-verified TCP/IP stack might be
> a bit of overkill. For example, "a friend of mine" have done this
> with severely ACSL-annotated C code and Frama-C couple years ago.

A formal semantics for both TCP/IP and for the sockets kernel
interface used on most flavors of Unix does exist:

https://www.cl.cam.ac.uk/~pes20/Netsem/paper3.pdf

It's written in Isabelle/HOL though I imagine it could be
mechanically translated into other systems like Coq with some effort.

I've heard that a formally verified TCP/IP stack had been attempted
subsequent to that but I haven't been able to rapidly confirm if that
was a real thing or memory problems on my part.

Perry
-- 
Perry E. Metzger		perry at piermont.com