[Cryptography] Formal Verification
Perry E. Metzger
perry at piermont.com
Fri Mar 18 17:55:21 EDT 2016
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
More information about the cryptography
mailing list