About Heartbleed, Memory Safety, CRASH/SAFE, HardBount/Watchdog, miTLS, and Everything Else

April 13, 2014

Heartbleed exploits a memory safety violation. One can break up such violations in many ways: spatial vs. temporal violations, control flow hijacking vs. no control data-only attacks, and for data-only attacks data corruption vs. data leaks. Heartbleed is a confidential data leak caused by a spatial memory violation (an out of bounds read). Here is a breakdown of memory safety violations and how Heartbleed fits in the rest of the picture:

Read the rest of this entry »

Learning/Teaching Coinduction with Coq

December 23, 2012

This semester Benjamin Pierce gave a course on Advanced Coq Martial Arts based on Adam Chlipala’s CPDT book. The course was very interactive, with the students giving most of the lectures and being in charge of creating the exercises. Since I wanted to know more about coinduction I taught the coinduction lectures and learned a lot in the process. One of the results of these lectures is a new set of materials for teaching coinduction in Coq:

These materials are based on Adam’s book chapter, Giménez and Castéran’s tutorial, and Xavier Leroy and Herve Grall’s development on coinductive operational semantics. I’ve tried my best to explain things better and to add good exercises.

Another result is a new Coq tactic that allows for aggressive automation of coinductive proofs. Most of the easy proofs now take the form coind using coind_principle; crush.

Update 2012-12-25:
Read the rest of this entry »

Expi2Java 1.6 Released

May 13, 2011

Alex Busenius and me are pleased to announce that Expi2Java 1.6 was released two days ago. And by the way, Alex has recently finished his MSc and is looking for a job in industry. If you know anything interesting in a German or English speaking country, please let him know.

Expi2Java 1.6 was released yesterday (11.05.2011)

The highlights of this release are the new symbolic library and a mechanized formalization in Coq.

The symbolic library abstracts away cryptographic primitives as symbolic terms and networking as pi-calculus-like channels. It is designed to be sound and simple enough to simplify proving the transformation secure. Both the symbolic and concrete libraries can be used interchangeably with all provided examples.

We have formalized the transformation from Expi Calculus to a subset of Java performed by Expi2Java using the Coq proof assistant and proved the symbolic library and the produced Java code to be well-typed. The formalization and all proofs can be found on the project homepage.

The full list of changes: Read the rest of this entry »

The ICFP 2010 talks are online

November 11, 2010

The ICFP 2010 talks are online for some days … hours and hours of home entertainment! Here is the presentation of my favorite ICFP 2010 paper:

And here is my own stressed and tired talk (for a less stressed version see this):

It’s amazing how much you can learn from a video of your own talk. So many times your impression as a speaker about what the audience got out of your talk are completely off. I wish more conferences would record talks, then maybe the talks would get better.

DVerify 1.0 released

September 23, 2010

DVerify is a new tool for verifying Dminor programs. It achieves pretty much the same thing as the Dminor type-checker, just in a quite different way: DVerify translates Dminor programs into a quite standard while language, and then uses the Boogie generic verification condition generator backend to verify the translated program. The soundness of this technique has been proved formally using Coq. DVerify and the Coq proofs are the product of Thorsten Tarrach’s recently defended Master’s thesis.

Dminor 0.1.1 released

September 20, 2010

Today we released version 0.1.1 of Dminor, our type-checker for a subset of the code name “M” Modeling Language. This brings several bug fixes and a couple of optimizations to our semantic-subtyping-based prototype type-checker. Andy Gordon posted about the original release of Dminor in December.

A Hoare logic for call-by-value functional programs

September 8, 2010

“Computational functions are reflected, at the logical level, as pairs of a precondition and postcondition. […] A function’s precondition and postcondition alone determine how it is lifted: its code is ignored. (The conformance of a function’s body to its declared pre- and postcondition
is checked, of course, via a proof obligation […]) This reflects a philosophy in which the only way of reasoning about the behavior of a function value is via its specification: code never appears within formulae.” — It seems that it took a very long time until this extremely natural idea was finally incorporated in a decent Hoare logic for functional programs (and a couple more years until it finally reached the world of refinement type systems 😉 )

“In this paper, we […] allow specifications to be expressed in higher-order logic. The intuitive justification for this approach is that, if functions can abstract over functions, then specifications must abstract over specifications.”