Hacker News Reader

Comment by gpcz | Hacker News Reader

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?

View on HN

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.

That's the way seL4 was written.

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.

Rust (http://www.rust-lang.org/) is a serious effort to build a language that's close to metal like C but safe.

Rust (http://playrust.com/) is a serious effort to build an envrionment that's about survival and gratuitous male nudity.

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].

1. Jeff Moser. Towards Moore's Law Software: Part 3 of 3. https://www.youtube.com/watch?v=UzjfeFJJseU

2. Occupy Babel!. http://www.cs.dartmouth.edu/~sergey/langsec/occupy/

3. Meredith Patterson. LANGSEC 2011–2016. https://www.youtube.com/watch?v=UzjfeFJJseU

Reply on news.ycombinator.com