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

Verifying Security Protocols and their Implementations

Last week I gave a two hour talk in our reading group about the verification of security protocols and their implementations. While the first half of my talk was a quite gentle introduction to protocol analysis, the second was actually much more interesting since I presented a nice paper from CSFW 2006:

Verified Interoperable Implementations of Security Protocols. Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Stephen Tse

The slides I used are available (pdf). They are “built” from the slides Andy Gordon used for his lecture at Marktoberdorf 2006 (pdf), the ones that Cédric Fournet used in a Colloquium talk at INRIA in 2007 (pdf), and the slides of one of the Language-based Security lectures Matteo Maffei gave last year at Saarland University (pdf).

Low-Level Software Security

Today I presented two papers in the System Security Seminar:

• Low-Level Software Security: Attacks and Defenses, by Úlfar Erlingsson (FOSAD 2007)
• Control-flow integrity, by Martín Abadi, Mihai Budiu, Úlfar Erlingsson, Jay Ligatti (CCS 2005)

The slides available here. They are for the most part based on Úlfar’s tutorial talk at FOSAD 2007.