! 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 !
Submission: April 10, 2013
Notification of acceptance: April 30, 2013
Final papers: May 31, 2013
Invited speaker: Boris Koepf, IMDEA, Spain
Read the rest of this entry »
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 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.
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 conﬁgurations. Expi2java is highly customizable, easily extensible and generates interoperable Java code. We show the ﬂexibility 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.
“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?”
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?
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:
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).