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:

Community vs. Corporation and Corrupt Politicians

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!

Pască Tanti Vali (traditional Romanian cheesecake)

This is actually 3 recipes in one, hopefully it’s not too complicated.

Tiramisu

Ingredients:

• 6 egg yolks
• 6 spoons of sugar
• 400g lady fingers
• 400g Mascarpone cheese
• 500g whipped cream
• 2 small bags of vanilla sugar (2 x 7-9g)
• some cacao
• amaretto liquor
• 10 little cups of espresso (or decaf espresso, or instant espresso) mixed with 4 tea spoons of sugar

Equipment:

• a high rectangular plastic/glass tray

Preparation:

• Make the coffee, add the 4 tea spoons of sugar and let it cool down.
• Stir the yolks with the sugar in a large container until the sugar melts, then add the cheese little by little.
• Whip the cream in a separate container. Keep 1/3 of it for decorating and incorporate the remaining 2/3 little by little into the cream.
• Pass the ends of the lady fingers quickly through the coffee, then put into the tray. Once you’re done with a complete layer of lady fingers pour half of the cream, then lay another layer of lady fingers rotated by 90 degrees (perpendicular wrt the first layer). Then put the other half of the cream and at the end the 1/3 of the whipped cream.
• Put in the fridge for a couple of hours.
• Before serving, put cacao on top through a small sieve.

Wealth Inequality in America

I wonder how Europe compares to all this …

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
===============
 

Pâté à la Valironrons

Here is a wonderful pâté recipe we have from our French friends. You need a meet grinder, but otherwise it’s not hard to make.

Ingredients (1 pound ~= 450g):

• 1 pound of chicken liver (or of any other poultry)
• 1/2 pound of bacon
• 1/2 pound of boneless pork
• 1 big bunch of parsley
• 1 egg
• 8g of salt (1/2 tablespoon)
• and then, at wish: black pepper, garlic, mustard, coriander (cilantro), juniper, clove, pistachios,…

Preparation: Grind everything*, homogenize, and put in a rectangular baking dish. Cook in the oven in a bain-marie for about 1h:30min at 380F (~193C). Cool down before serving.

[*] Grinding chicken liver works best if it’s slightly frozen, otherwise the process is a bit messy.

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.

Learning/Teaching Coinduction with Coq

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:

• An Introduction to Coinduction
• Coinductive Operational Semantics

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.

• Full Coq development including my coind tactic

Update 2012-12-25: