Official LSV Web Site

LSV Secsi

Presentation

Key words : Static analysis, abstract interpretation, C code analysis, pointer analysis, cryptographic protocols analysis, cryptographic protocols analyzer, Horn clauses, First order logic.

Csur is a project about automatic analysis of cryptographic protocols written in C. Csur uses a new hybrid analysis of C code: programs represent roles of agents in protocols and a static analysis computes message exchange between agents of protocols. Secrecy properties of protocols can be analyzed using a Dolev-Yao model. Bugs in the implementation can also be found using our techniques. Csur comes with 2 tools: csurcc is a compiler and a control flow graph generator, csurrun is the analyzer and performs cryptographic protocols analysis.

History

Csur was started before SECSI was created, early 2002. It is developed by Fabrice Parrennes, once a postdoc on the ACI jeunes chercheur "Sécurité informatique, protocoles cryptographiques et détection d'intrusion", attributed to Jean Goubault-Larrecq in 2001. Since September 01, 2003 Fabrice Parrennes has been part-time teaching assistant at ENS Cachan.

Csur was initially the basis for a homework assignment to students of the static analysis course at DESS "Développement de logiciels sûrs" (see original page (in French) ), which counted as their final grade. This version of Csur was a static analyzer of C programs, written in OCaml, which detected arithmetic overflows, illegal memory accesses (array bounds overflow notably). It was written by Jean Goubault-Larrecq. Then, only specific modules were provided to students, the rest being only available to them in compiled form. The assignment was for students to rewrite the missing sources according to specification.

This first version of CSur served as a foundation for the new Csur Project, started in 2002 by Fabrice Parrennes under the direction of Jean Goubault-Larrecq. The new Csur Project is meant to detect cryptographic protocol-related vulnerabilities in "C" source code. It's parses, analyses C source files, then produces List of Horn clauses that can be passed on to tools like SPASS or H1 to detect plausible attacks, or better, to prove formally that the input C program is secure. The basic idea is that Horn clauses can be used to represent both interaction with the network, in Dolev-Yao style, and to describe in-memory pointer aliasing. For example, calls to the write(2) primitive will trigger the generation of a clause of the form knows(M)<=... where M is the message written to the network, ans calls to the read(2) primitive triggers clauses P(X) <= knows(X) where knows is the predicate recognizing all messages known to a Dolev-Yao intruder, and which is axiomatized as in classical Dolev-Yao analysis of cryptographic protocols. On the other hand, points-to analyses (see Andersen and Steensgaard analyses) can also be recast as generating Horn clauses.

As an example of what Csur can analyze, see the following piece of C code. This is a working implementation of role A of the Needham-Schroeder public-key protocol, contributed by Julien Olivain and Fabrice Parrennes. 



01| #include <openssl/bn.h>
02| #include <openssl/rand.h>
03| #include "needham_type.h"
04| /* [Omitted other #includes] */
05|
06| int main(int argc, char **argv) {
06|   int conn_fd; // The communication socket.
07|   char alice[30]; // A's name
08|   int  alice_port;
09|   char bob[30];   // B's name as seen from A.
10|   int  bob_port;
11|   // Temporaries:
12|   unsigned char nonceA[16];
13|   char temp[1024];
14|   // Messages:
15|   msg_t alice_mess_1; BIGNUM *cipher_1;
16|   msg_t alice_mess_2; BIGNUM *cipher_2;
17|   msg_t alice_mess_3; BIGNUM *cipher_3;
18|   // Keys:
19|   struct nskey_s *alice_key;
20|   struct nskey_s *bob_key;
21|   alice_key = malloc (sizeof(struct nskey_s));
22|   bob_key   = malloc (sizeof(struct nskey_s));
23|   /* [Omitted code] generate A's and B's keys
24|      in alice_key and bob_key. */
25|   // Initialization:
26|   alice_port = PORT_ALICE;
27|   strcpy(alice,"127.0.0.1");
28|   strcpy(bob,argv[1]); bob_port = atoi(argv[2]);
29| 
30|   // Open connection to B:
31|   conn_fd = connect_socket(bob, bob_port);


32|   /*** 1. A -> B : {Na, A}_pub(B) ***/
33|   // Create A's nonce Na:
34|   RAND_bytes(nonceA, 16);
35|   alice_mess_1.msg_type = MSG1;
36|   alice_mess_1.msg.msg1.id = ALICE_ID;
37|   memcpy(alice_mess_1.msg.msg1.nonce,
38|          nonceA, sizeof(nonceA));
39|   // Encrypt and get {Na, A}_pub(B)
40|   cipher_1 = BN_new();
41|   my_cypher( &alice_mess_1, bob_key, cipher_1);
42|   write(conn_fd, BN_bn2hex(cipher_1), 128);
43| 
44|   /*** 2. B -> A : {Na, Nb}_pub(A) ***/
45|   cipher_2 = BN_new();
46|   read(conn_fd, temp, 128);
47|   BN_hex2bn(&cipher_2, temp);
48|   // Decrypt and get Na, Nb:
49|   my_decypher(cipher_2, alice_key, &alice_mess_2);
50|   // Check that Na is the expected one:
51|   if (strncmp(alice_mess_2.msg.msg2.nonce1,
52|               nonceA , sizeof(nonceA)))
53|     exit (1);
54| 
55|   /*** 3. A -> B : {Nb}_pub(B) ***/
56|   alice_mess_3.msg_type = MSG3;
57|   memcpy(alice_mess_3.msg.msg3.nonce, 
58|          alice_mess_2.msg.msg2.nonce2,
59|          sizeof(alice_mess_2.msg.msg2.nonce2));
60|   cipher_3 = BN_new();
61|   my_cypher( &alice_mess_3, bob_key, cipher_3);
62|   write(conn_fd, BN_bn2hex(cipher_3), 128);
63|   return 0;
64| }

Figure 1: A sample C implementation of the NS protocol

The specification of the actual protocol, in standard notation, is included in comment of the form /*** ... ***/(2) (right column), so as to let the reader appreciate the semantic gap between the (idealized) protocol and the C code that implements it.

The challenge here is in the subtle interaction between the Dolev-Yao world and the C pointer world. At the end of 2003, CSur is a functionnal prototype (see Related Tools).

Some references

People

People actually working in this project are members of SECSI Team .

In particular, active members are :

Jean Goubault-Larrecq (In charge, Full Professor, ENS Cachan)
Fabrice Parrennes (Main developer, Part-time teaching and research assistant, Cachan)
Mathieu Baudet (PhD student, LSV INRIA)
Julien Olivain (Project engineer, INRIA)


SECSI is a common project of the INRIA Futurs research unit, of the LSV (CNRS UMR 8643), at the ENS Cachan. See also the project page at INRIA.

Documentation

Download

The compiler and tools are distributed under copyright license. A beta version will be soon available.

© Copyright Fabrice Parrennes, March 2004

About LSV