Expi2Java 1.6 Released

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:

DVerify 1.0 released

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.

Dminor 0.1.1 released

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.

zk-typechecker 0.2.0 Released

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.

Smile Shutter

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)

The Debian Patch for OpenSSL

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?

Perfect Secrecy ;)

OTP: An Encoder/Decoder For One-Time Pads written by Karl Fogel.

Skype Plugin for Gaim/Pidgin/Adium

The URL: http://www.myjobspace.co.nz/images/pidgin/

The good. This is a plugin many people (me included) have been waiting for years. Most important, it allows you to have all your buddies in one place, and communicate with them in a stemless way (no matter whether they use GTalk, Yahoo!, AIM, ICQ, MSN, IRC, or whatever). This has always been one of the biggest advantages of using Gaim/Pidgin/Adium. But there was still one important protocol which it could not do, because the developers of this protocol tried their very best to make this impractical: Skype. Still, a while ago, in a sudden outbreak of common sense, the Skype developers released a public API, which now made this plugin possible.

The bad. The plugin requires Skype to be running as it uses the Skype public API to communicate with a running copy of Skype. This is needed since reverse-engineering the evil Skype protocol, while not impossible, would be a daunting task (see Silver Needle in the Skype for more details about this).

Many people are using Gaim/Pidgin/Adium because it is Free Software (GPL). It is also running in more or less the same way on any operating system. This is particularly interesting for people using proprietary instant messaging clients on non-Windows machines, because they had to stick with much older versions (while for Windows, Skype is at version 3.6, for Linux it is at 1.4 and for Mac at 2.6), this assuming there was some version for their operating system. These are problems that the current plugin can unfortunately not fix, since it relies on a running (proprietary and possible outdated) copy of Skype. Still, the plugin itself is GPL.

The uggly. No voice or video support, but this is a general problem with Gaim/Pidgin/Adium, which will only get solved if someone is willing to invest some time into it. The plugin itself worked fine for me so far with Adium, even though there are some Known Issues (see readme).

Related (good) news: GTalk now interoperates with AIM and ICQ.

Apple releases broken update

Updating Mac OS X to 10.4.10 also updates QuickTime to 7.2, which if your on an Intel Mac will very likely cause all your Rosseta applications to stop working. There is an official fix which is not only involved, but it sometimes does not work. You might get this error when running update_prebinding:

dyld: re-prebound: 0x90bee000 /usr/lib/libgcc_s.1.dylib
update_prebinding: error: dependent dylib is not prebound
update_prebinding: error 256 running update_prebinding_core

Then you need to follow the instructions here.

Some people in the Apple QA team should get a kick in the balls for this.

muCommander is Now Free Software

… under the GPL version 3.