Gran: grsecurity analyser

Our paper about automated analysis of grsecurity has been accepted for presentation at IEEE CSF 2012 at the end of June. In the paper we formalize grsecurity semantics and, based on that, we develop a tool that checks for security flaws inside real grsecurity policies. The paper is based on Marco Squarcina’s undergraduate thesis (tesi triennale).

The gran tool (grsecurity analyser) is available for download here.

c00kies@venice got third place in UCSB iCTF

Logo c00kies@venicec00kies@venice is our nickname for computer security competitions. Last night, we got third place in UCSB iCTF 2010 , the biggest international “Capture The Flag” in the world.This year 72 teams (900 students) from 16 countries competed in the game. It was a great game of hacking and challenge-solving perfectly organized by Giovanni Vigna at the University of California, Santa Barbara (that we thank!).

We are very very proud and happy! More information (including pictures) will be soon available, stay tuned!

Security APIs at FOSAD school

I ve just given a course at the FOSAD’10 school, reviewing practical attacks on security APIs and illustrating formal techniques to detect and fix them. The first part of the course focusses on PIN cracking attacks on Hardware Security Modules (HSMs) used by ATM networks to protect user PINs. The second part focusses on PKCS#11 tokens. I have described Tookan, a tool that reverse engineers real cryptographic tokens and performs a formal analysis of the resulting model, finding possible attacks and testing them on the real device (hope to have soon a trial version on this site). I have finally  illustrated CryptokiX, our security-enhanced software simulator of a PKCS#11 token. Here are the slides [Part I] [Part II]