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 »
September 23, 2010
DVerify is a new tool for verifying Dminor programs. It achieves pretty much the same thing as the Dminor type-checker, just in a quite different way: DVerify translates Dminor programs into a quite standard while language, and then uses the Boogie generic verification condition generator backend to verify the translated program. The soundness of this technique has been proved formally using Coq. DVerify and the Coq proofs are the product of Thorsten Tarrach’s recently defended Master’s thesis.
September 20, 2010
Today we released version 0.1.1 of Dminor, our type-checker for a subset of the code name “M” Modeling Language. This brings several bug fixes and a couple of optimizations to our semantic-subtyping-based prototype type-checker. Andy Gordon posted about the original release of Dminor in December.
February 12, 2009
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.
July 12, 2008
Found out about a funny feature in some of the new cameras from Sony: the Smile Shutter. It can measure the smile of your subjects and take a picture only they are properly smiling.
I wonder whether I can go over 100% 🙂 One of my friends has such a camera, so we will give it a try soon. Hope it doesn’t explode 🙂
I also wonder about the future evolution of this feature; what is it going to do? Detect fake smiles? sarcastic smiles? evil smiles? wistful smiles? retail smiles? stewardess smiles? …
(I found out about this feature from the blog of a friend)
May 16, 2008
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?