Towards Formal Verification of Contiki: Analysis of the AES–CCM* Modules with Frama-C

Conference object, Other literature type English OPEN
Peyrard, Alexandre; Kosmatov, Nikolai; Duquennoy, Simon; Raza, Shahid;

International audience; The number of Internet of Things (IoT) applications is rapidly increasing and allows embedded devices today to be massively connected to the Internet. This raises software security questions. This paper demonstrates the usage of formal verificati... View more
  • References (18)
    18 references, page 1 of 2

    [1] E. Alkassar, E. Cohen, M. Kovalev, and W. J. Paul. Verification of TLB virtualization implemented in C. In Proc. of the 4th International Conference on Verified Software: Theories, Tools, Experiments (VSTTE 2012), volume 7152 of LNCS, pages 209-224. Springer, 2012.

    [2] E. Alkassar, W. Paul, A. Starostin, and A. Tsyban. Pervasive verification of an OS microkernel. In Proc. of the 3rd International Conference on Verified Software: Theories, Tools, Experiments (VSTTE 2010), volume 6217 of LNCS, pages 71-85. Springer, 2010.

    [3] C. Barrett, C. L. Conway, M. Deters, L. Hadarean, D. Jovanovic, T. King, A. Reynolds, and C. Tinelli. CVC4. In Proc. of the 23rd International Conference on Computer Aided Verification (CAV 2011), volume 6806 of LNCS, pages 171-177, 2011.

    [4] G. Barthe, G. Betarte, J. D. Campo, J. M. Chimento, and C. Luna. Formally verified implementation of an idealized model of virtualization. In Proc. of the 19th International Conference on Types for Proofs and Programs (TYPES 2013), pages 45-63, 2013.

    [5] P. Baudin, P. Cuoq, J.-C. Fillitre, C. March, B. Monate, Y. Moy, and V. Prevosto. ACSL: ANSI/ISO C Specification Language.

    [6] E. Biham and A. Shamir. Differential Cryptanalysis of the Data Encryption Standard. Springer, 1993.

    [7] A. Blanchard, N. Kosmatov, M. Lemerre, and F. Loulergue. A case study on formal verification of the anaxagoros hypervisor paging system with frama-c. In Proc. of the 20th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2015), volume 9128 of LNCS, pages 15-30. Springer, June 2015.

    [8] S. Conchon et al. The Alt-Ergo Automated Theorem Prover.

    [9] J. Daemen and V. Rijmen. The Design of Rijndael: AES - The Advanced Encryption Standard. Information Security and Cryptography. Springer, 2002.

    [10] L. de Moura and N. Bjørner. Z3: An efficient SMT solver. In Proc. of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008), pages 337-340. Springer, 2008.

  • Metrics
Share - Bookmark