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:
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!
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 »
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.
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.
Read the rest of this entry »
- Universitatea Babeş-Bolyai, Cluj Napoca
- Universitatea Alexandru Ioan Cuza, Iaşi
- Universitatea Valahia, Târgovişte
- Universitatea Bucureşti, Bucureşti
- Universitatea Politehnica Bucureşti
As always take this ranking with a big grain of salt.
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 »