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

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:

Moving to Paris

It’s official (for a while now, but the blog is constantly neglected): we’re moving to Paris on the 1st of October! After a strenuous academic job search in Europe that started last October, things are finally settled: I accepted a researcher position at INRIA Paris-Rocquencourt. The position is called  “chargé de recherche (CR)” in French, is permanent, and seems to offer perfect job security (French civil servant position). And given that this is INRIA, the competition was fierce, and also painful, since some of the competitors are good friends, who are, as US people might put it, at least as awesome as I am.

The INRIA team I’ll be joining focuses on security (security protocols and web security in particular). And to make things even better, the team is located at Place d’Italie in the center of Paris. We already got a short-term lease for an apartment that’s close to Place d’Italie for the first 2 months, but getting a long term lease in Paris afterwards is going to be a big challenge. Beate’s French skills will help a lot, and I hope to start learning French really soon now (at the moment I only know a tiny bit of culinary French).

Anyway, starting on Friday we’re going on a big adventure trip to many cool US national parks (Zion, Grand Canyon, Bryce, Grand Teton, Yellowstone, and Glacier) and taking the last chance to enjoy the wonderful nature here. Our stay in the US was awesome, but we are also very happy to return to our many cool friends and family in Europe. So long, and thanks for all the fish!

CFP: FCS’13 Workshop on Foundations of Computer Security

My first PC membership 🙂

+---------------------------------------------------------+
!                                                         !
!			FCS 2013                          !
!       Workshop on Foundations of Computer Security      !
!     Tulane University, New Orleans, Louisiana, USA      !
!                     June 29, 2013                       !
!   http://prosecco.inria.fr/personal/bblanche/fcs13/     !
!                                                         !
!          Affiliated with LICS 2013 and CSF 2013         !
!                                                         !
+---------------------------------------------------------+

Important dates
===============

Submission:			April 10, 2013
Notification of acceptance: 	April 30, 2013
Final papers: 			May 31, 2013

Invited speaker: Boris Koepf, IMDEA, Spain
===============
 

All Your IFCException Are Belong To Oakland 2013

Our paper marrying reliable exception handling and sound fine-grained dynamic information flow control was accepted at the IEEE Symposium on Security & Privacy (Oakland 2013).

All Your IFCException Are Belong To Us. Cătălin Hriţcu, Michael Greenberg, Ben Karel, Benjamin C. Pierce, Greg Morrisett.

• Coq formalization and proofs are available here.
• Breeze interpreter, libraries, and sample applications are available here.
• A previous version of this work was called Exceptionally Available Dynamic IFC, July 2012.

Expi2Java 1.6 Released

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:

zk-typechecker 0.2.0 Released

The zero-knowledge type-checker is a tool for automatically analyzing the security of protocols that use zero-knowledge proofs. The analysis is modular and compositional, and provides security proofs for an unbounded number of protocol executions. The type-checker relies on the SPASS (or E) automated theorem prover to discharge proof obligations. It is released under the terms of the Apache License.

This release of the zero-knowledge type-checker adds support for security despite compromise and fixes many of the issues in the initial release (release notes). You can grab it from the page of the project.

My First Students

Last week two of the students I supervise submitted their Bachelor’s Thesis. Both theses are about automatically generating executable code from abstract specifications of security protocols, however, the focus is quite different. While Alex worked on a very powerful tool that generates interoperable protocol implementations (to be released soon), Thorsten formalized a much simpler code generator and proved it to the preserve the security of the original protocol. In the future we would like of course to have both, the extensibility, flexibility and interoperability of Alex’ tool, with the same strong security guarantees as Thorsten proves for his generated code.

• Expi2Java – An Extensible Code Generator for Security Protocols (Alex Busenius)
  Abstract: This thesis presents expi2java, an extensible code generator for security protocols. We use a variant of Spi calculus for the protocol specifications and complement it with an expressive type system that is designed to reject inconsistent protocols. This type system features subtyping and parametric polymorphism. It is able to handle the types of nested terms, specialized channels and even low-level term configurations. Expi2java is highly customizable, easily extensible and generates interoperable Java code. We show the flexibility of our approach by generating an implementation of the Transport Layer Security (TLS) protocol.
• Spi2F# – A Prototype Code Generator for Security Protocols (Thorsten Tarrach)
  Abstract: This thesis describes a new prototype tool that automatically generates a secure F# implementation of any protocol described in the Spi calculus. Type systems were previously proposed for analysing the security of both Spi calculus processes and F# implementations. The thesis investigates a formal translation from the Spi calculus to F# that is proved to preserve typability, and therefore the security properties of the original protocol are preserved.

The Debian Patch for OpenSSL

A Slashdot comment linked to this very interesting post by a Debian developer on the openssl-dev list:

“What I currently see as best option is to actually comment out those 2 lines of code. But I have no idea what effect this really has on the RNG. The only effect I see is that the pool might receive less entropy. But on the other hand, I’m not even sure how much entropy some unitialised data has.

What do you people think about removing those 2 lines of code?”

This change made all keys generated over the last 2 years on any machine running Debian (or a derivative) be extremely easily guessable. Not only should you regenerate all your keys as soon as possible if affected, but if somebody recorded sensitive traffic you did in the last two years then you are in deep deep trouble.

Why on earth are the Debian developers patching security-critical packages without having absolutely any clue about the implications? How many other vulnerabilities did they actually introduce in this way?

Perfect Secrecy ;)

OTP: An Encoder/Decoder For One-Time Pads written by Karl Fogel.

Two Hardware Hacks from Princeton

Cold Boot Attacks on Encryption Keys

The paper and more materials

 
 

Security Analysis of the Diebold AccuVote-TS Voting Machine

The paper and more materials

In more recent news: Diebold voting machine key copied from pic on Diebold site