I've been thinking recently about Heartbleed, and I was wondering if by writing C code to implement various network and cryptographic protocols, we're acting as human compilers for something that might be better represented in a more abstract format. I know there's some research on this already (the Austin Protocol Compiler), but does anyone here know of any other serious efforts to take the human out of the equation in terms of implementing protocols in C?
There are efforts by Microsoft Research in this direction:
http://research.microsoft.com/en-us/projects/slam/
They have developed several ___domain specific languages and specification tools for developing drivers. I think similar methods are applicable to protocols.
The most viable option today seems to be writing code in some language with strong formal guarantees (Agda, Coq) with extracting to Haskell/OCaml for generating C code from there.
I think gpcz was suggesting something more along the lines of an entirely new approach to protocol implementation, like VPRI's TCP/IP stack that Jeff Moser describes[1], rather than just swapping out C for something else while keeping the hand-written aspect.
> Let's say we want to build the TCP/IP stack of an operating system. A traditional implementation might take 10,000 lines of code. What if you rethought the design from the ground up? What if you could make the IP packet handling code look almost identical to the RFC 791 diagram which defines IP?
If the industry as whole could agree on this approach in a move similar to the Dijkstra/structured programming move that happened a few decades back, the sort of verifiable interoperability + security that Meredith Patterson and Sergey Bratus (who you may recognize from Occupy Babel![2]) call for would be closer to reach[3].
C is only used because for cryptography we really need to be close to the CPU and memory, going all assembler is an option actually. Anything higher than that and you have to have formal proofs for your compiler as well as your equations.
Don't listen to him, its just for performance, compatibility and portability. There's many other reasons why you might want to use another language, and some do.
