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 »


Moving to Paris

July 24, 2013

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

February 25, 2013

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
 Read the rest of this entry »

All Your IFCException Are Belong To Oakland 2013

February 16, 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.

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 »

Research Ranking of Romanian Universities 2011

July 11, 2011

The “Alexandru Ioan Cuza” University from Iaşi scored second in the 2011 Computer Science scientific results ranking:

  1. Universitatea Babeş-Bolyai, Cluj Napoca
  2. Universitatea Alexandru Ioan Cuza, Iaşi
  3. Universitatea Valahia, Târgovişte
  4. Universitatea Bucureşti, Bucureşti
  5. Universitatea Politehnica Bucureşti

As always take this ranking with a big grain of salt.

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 »