The long, hard road from theoretical security to practical security is one that has received a lot of attention this year at Real World Crypto. We’ve had Moti Young remind of us of Adi Shamir’s words that “crypto is dead” because of practical considerations due to APTs, Bruce Schneier reassure us that the NSA is not capable of mathematic magic and has probably been using practical security holes to read data that should theoretically be unreadable and Douglas Stebila show us how that all known attacks against TLS have been against its implementation and never against the cryptographic primitives themselves.
A common theme seems to be repeating itself here in New York. Namely that the main problems in cryptographic implementation today are not to do with the security of the primitives but with the engineering. You may have an algorithm for which all the mathematics point towards a highly secure cryptographic scheme but if the implementation of that scheme leaks its state, the security that was proved in theory means nothing. So was there any good news this year at Real World Crypto for theoreticians lamenting the downfall of the cryptographic algorithms they took so long to prove secure because of engineering and implementation? Well, according to Francois Dupressoir there is.
In a talk entitled “Efficient Provably Secure Machine Code from High-Level Implementations” Francois presented his paper [1] with the same title in which a method of ensuring that the proven theoretical security of an algorithm can be carried through to its machine code representation. The method described for doing this was twofold. 1. Ensuring that the high level language (C in this case) is a secure representation of the algorithm and that there is no leakage beyond what is specified in the security definition. 2. That the code is compiled in such a way that the semantic correctness of the high level code (not just its consistency) is strongly maintained in the machine code.
The first of these was done using EasyCrypt to prove the security of the C code. EasyCrypt is an SMT-based interactive prover geared towards proving the security properties of cryptographic schemes. This was extended with a number of libraries to lower the level of abstraction of specifications and run to ensure that the C code is written to a specified definition of security. The main aim of this was to make the C code secure (as defined in the cryptographic scheme specifications) against idealized probabilistic operations in an enhanced security model where it is assumed that the attacker has access to execution traces meant to capture side channel leakage. This enabled the authors to claim that the C code had the same level of security as defined in the theoretical model of the encryption scheme.
Following the development of provably secure C code the second stage was to compile it into equally secure machine code. To do this the authors sought to strongly maintain the correctness (semantic preservation) of the C code using CompCert. CompCert is formally verified optimising compiller which has the proven capability of producing machine code with stong correctness and reasonable efficiency when compared with other general purpose C compilers. By using CompCert to maintain the correctness of the EasyCrypt tested C code, the resulting machine code could be taken to have the same security properties as the C code, which had previously been shown to have the same level of security as the theoretical encryption scheme.
This means that the level of security that was proved originally in theory for the encryption scheme can be proved for the machine code implementation of it, or to put it another way the security of the scheme can be proven from pencil to processor.
[1] Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations. Jose Bacelar Almeida, Manuel Barbos, Gilles Barthe, Francois Dupressoir. 2013.
A common theme seems to be repeating itself here in New York. Namely that the main problems in cryptographic implementation today are not to do with the security of the primitives but with the engineering. You may have an algorithm for which all the mathematics point towards a highly secure cryptographic scheme but if the implementation of that scheme leaks its state, the security that was proved in theory means nothing. So was there any good news this year at Real World Crypto for theoreticians lamenting the downfall of the cryptographic algorithms they took so long to prove secure because of engineering and implementation? Well, according to Francois Dupressoir there is.
In a talk entitled “Efficient Provably Secure Machine Code from High-Level Implementations” Francois presented his paper [1] with the same title in which a method of ensuring that the proven theoretical security of an algorithm can be carried through to its machine code representation. The method described for doing this was twofold. 1. Ensuring that the high level language (C in this case) is a secure representation of the algorithm and that there is no leakage beyond what is specified in the security definition. 2. That the code is compiled in such a way that the semantic correctness of the high level code (not just its consistency) is strongly maintained in the machine code.
The first of these was done using EasyCrypt to prove the security of the C code. EasyCrypt is an SMT-based interactive prover geared towards proving the security properties of cryptographic schemes. This was extended with a number of libraries to lower the level of abstraction of specifications and run to ensure that the C code is written to a specified definition of security. The main aim of this was to make the C code secure (as defined in the cryptographic scheme specifications) against idealized probabilistic operations in an enhanced security model where it is assumed that the attacker has access to execution traces meant to capture side channel leakage. This enabled the authors to claim that the C code had the same level of security as defined in the theoretical model of the encryption scheme.
Following the development of provably secure C code the second stage was to compile it into equally secure machine code. To do this the authors sought to strongly maintain the correctness (semantic preservation) of the C code using CompCert. CompCert is formally verified optimising compiller which has the proven capability of producing machine code with stong correctness and reasonable efficiency when compared with other general purpose C compilers. By using CompCert to maintain the correctness of the EasyCrypt tested C code, the resulting machine code could be taken to have the same security properties as the C code, which had previously been shown to have the same level of security as the theoretical encryption scheme.
This means that the level of security that was proved originally in theory for the encryption scheme can be proved for the machine code implementation of it, or to put it another way the security of the scheme can be proven from pencil to processor.
[1] Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations. Jose Bacelar Almeida, Manuel Barbos, Gilles Barthe, Francois Dupressoir. 2013.
No comments:
Post a Comment