, Considérant un programme INIT; i:=0; WHILE(TEST_i) iteration_i; i++

. End_boucle, Montrer que la boucle termine. La technique consiste à trouver un variant, c'est-à-dire un entier V , positif au départ, dont on montre : 1. qu'il décroît (de façon entière) à chaque itération 2, Considérant une propriété ? que l'on veut vraie à la fin de la boucle

]. Zéro, ou moins) en un nombre fini d'itérations et par [2], à ce moment on ne pourra rester dans la boucle, Donc on sort de la boucle au bout d'un nombre fini d'itérations

, ?(i) dénote le fait que ? est vrai des variables locales au début de l'itération i. Et montrer -que l'initialisation établit ?, i.e. ?(0) -que les itérations intermédiaires préservent ?, i.e ?(i) & T EST_i ? ?(i + 1) -que ? à la dernière itération assure le résultat recherché, -Trouver un invariant de boucle, c'est-à-dire une propriété ? portant sur les variables locales

, 2 (des deux versions) sont équivalentes (c'est-à-dire equiv[M 1.initialisation ? M 2.initialisation]) dans le sens où partant de la même mé-moire après exécution de ces deux procédures le contenu des résultats est équivalents. Ce lemme garantie que les procédures d'initialisation ne touchent pas à la mémoire, Nous montrons le lemme nommé init qui énonce que les procédures d'initialisation d'une mémoire décrites dans les modules M 1 et M

, Nous donnons un autre prédicat encrypt_correct qui définit ce qu'un arbre correctement calculé

, pred encrypt_correct(m : memory, k : key, i : int, j : int) = mem(dom m)(i, j) ? m

, Ce prédicat énonce qu'étant données une mémoire, une adresse et une clé, si l'adresse appartient au domaine de la mémoire (mem(dom m)(i, j)) alors la donnée contenue à l'adresse du noeud père est égale à la valeur du condensé cryptographique de l'ensemble de ses fils Some

, Notons l'utilisation de l'opérateur Some ; EasyCrypt gère le type de données map à la manière du type d'Haskell Maybe

, Nous montrons que l'appel de la procédure d'initialisation du module M 1 sur une mémoire garantie après exécution de la procédure que la mémoire résultante est correctement chiffrée

. Remarquons, à la manière dont la procédure initialisation est codée dans le module M 1 nous n'avons pas accès à la mémoire, la procédure ne retourne aucun résultat (le résultat de type unit). Pour pallier ce problème et sans modifier le comportement de celle-ci nous ajoutons

, memory = { ?(i : int, j : int), 0 ? j ? 0 ? i < s ? encrypt_correct res M

, La preuve est donnée dans 5.3.5. Nous montrons le même lemme pour la procédure write du module M 2

, Nous montrons enfin un lemme, appelé Read, sur l'équivalence des procédures de lecture vérifiée verifyread

, equiv Read : M 1.verifyread ? M 2.verifyread : ={M.k, M.m} ? equiv_mem M.m{1} M.m{2} ? ?(i : int, j : int)

, Le lemme énonce que partant d'un même espace mémoire (ou équivalent) et d'une même clé, et que si les deux espaces mémoire sont correctement condensés alors le résultat de la lecture verifyread du module M1

, Le lemme Read garantie que dans le cas où il n'y a pas de corruption de la mémoire les deux procédures verifyread sont équivalentes dans le sens où elles retournent le même résultat

, Elle ne s'applique qu'au théorique, au sens ou aucune preuve mathématique ne peut garantir l'état physique du matériel. Qui plus est, cette étude à eu lieu sur des "proto-algorithmes", avant que les implémentations matérielles réelles soient fixées. Enfin, cette étude ne traite que du matériel SecBus, en ce sens qu'elle ne considère ni les logiciels (bootloader, applications...) utilisant les service offerts et l'intelligence de cette utilisation

. Le-module-de, voir page 114) est responsable du chiffrement et de déchiffrement des données transférées entre le SoC et ses mé-moires externes et de la gestion et la vérification de leur intégrité

, Nous présentons ici l'implémentation du HSM sur une carte à base de FPGA de la famille Zynq de Xilinx, vol.57

, Ces FPGA sont constitués de deux parties : -La partie Processing System (PS) qui contient notamment deux coeurs de processeur ARM, un contrôleur mémoire et quelques périphériques -La partie Programmable Logic (PL) qui contient une matrice FPGA programmable classique Ces deux zones communiquent entre elles grâce à plusieurs bus AXI

, L'espace d'adressage 32 bits des coeurs ARM est divisé en quatre zones de chacune 1 Gio

, La première permet d'adresser directement la mémoire physique via le contrôleur mémoire (lien AS0 dans la figure 5.6). Les deux zones suivantes permettent aux processeurs d'envoyer des requêtes vers la partie PL (via les deux bus AXI, AS1 et AS2 sur la figure), La dernière zone permet aux processeurs d'adresser les périphériques situés dans la partie PS et notamment la On-Chip Memory

Z. Le, Le logiciel s'exécutant sur la partie PS a été modifié de manière à utiliser la plage d'adresse AS2 au lieu d'AS0 pour accéder à la mémoire externe. Ainsi, toutes les transactions mémoires ont été déroutées via la partie PL où est implémenté le HSM, La figure 5.6 montre comment le HSM est inséré dans une plate-forme de prototypage à base de Zynq, vol.58

, Cette section présente les résultats de l'évaluation de performance du HSM sur la plateforme de démonstration

, Le tableau 5.5 résume l'utilisation des ressources occupées par le HSM sur le FPGA Xilinx Zynq-7020 de Xilinx de la carte ZedBoard

, Le Zynq-7020 étant le deuxième plus petit membre de la famille et un FPGA étant beaucoup moins dense qu'un autre circuit intégré à technologie équivalente, ces résultats peuvent être considérés comme très raisonnables. L'utilisation (généralement optimiste) du rapport de conversion de Xilinx peut être estimé à environ 750 k portes ou 3 M transistors. La fabrication du HSM dans un processus de 14 nm occuperait une surface de silicium d

. Bibliographie, Bank customer data sold on ebay

M. G. Kuhn, Cipher instruction search attack on the bus-encryption security microcontroller DS5002FP, IEEE Transaction on Computers, vol.47, issue.10, pp.1153-1157, 1998.
DOI : 10.1109/12.729797

J. Stern, La Science du secret, 1998.

A. J. Menezes, P. C. Van-oorschot, and S. A. Vanstone, Handbook of Applied Cryptography, 1996.

A. Kerckhoffs, La cryptographie militaire, Journal des sciences militaires, 1883, pp.5-38

, La cryptographie militaire, Journal des sciences militaires, 1883, pp.161-191

G. S. Vernam, Secret signaling system, United States Patent, US1310719A, 1919.

C. E. Shannon, Communication theory of secrecy systems, Bell system technical journal, vol.28, pp.656-715, 1949.

, Advanced encryption standard (aes), Processing Standards Publication 197, 2001.

, Data encryption standard (des), Processing Standards Publication FIPS PUB 46-2, 1993.

E. F. , Foundation, Cracking DES : Secrets of Encryption Research, Wiretap Politics and Chip Design, 1998.

A. Hodjat, D. D. Hwang, B. Lai, K. Tiri, and I. Verbauwhede, A 3.84 gbits/s aes crypto coprocessor with modes of operation in a 0.18 µm cmos technology, Proceedings of the 15th ACM Great Lakes symposium on VLSI (GLSVLSI'05), pp.60-63, 2005.

, Recommendation for block cipher modes of operation, Special Publication 800-38A, 2001.

M. E. Diffi, . Whitfield, and . Hellman, New directions in cryptography, Transactions on Information Theory, pp.644-654, 1976.

, A. method for obtaining digital signatures and public-key cryptosystems, Communications of the ACM, pp.120-126, 1978.

J. Mcloone and M. Mccanny, Fast montgomery modular multiplication and rsa cryptographic processor architectures, Proceedings of the 37th IEEE Computer Society Asilomar Conference on Signals, Systems and Computers, pp.379-384, 2003.

, Secure hash standard (shs), Federal Information Processing Standards Publication 180-2, 2002.

P. C. Kocher, Timing attacks on implementations of diffie-hellman, rsa, dss, and other systems, Advances in Cryptology -CRYPTO'96, vol.1109, pp.104-113, 1996.

P. C. Kocher, J. Joshua, and J. Benjamin, Differential power analysis, Advances in Cryptology -CRYPTO'99, vol.1666, pp.388-397, 1999.

E. Biham and A. Shamir, Differential fault analysis of secret key cryptosystems, vol.1294, pp.513-525, 1997.

R. Elbaz, D. Champagne, and R. B. Lee, The reduced address space (ras) for application memory authentication, pp.47-63, 2008.

R. Elbaz, L. Torres, G. Sassatelli, P. Guillemin, M. Bardouillet et al., A parallelized way to provide data encryption and integrity checking on a processor-memory bus, Proceeding of the 43rd ACM/IEEE Design Automation Conference, pp.506-509, 2006.
URL : https://hal.archives-ouvertes.fr/lirmm-00102783

C. Fruhwirth, New methods in hard disk encryption, 2005.

R. Elbaz, D. Champagne, C. Gebotys, R. B. Lee, N. Potlapally et al., Hardware mechanisms for memory authentication : A survey of existing techniques and engines, Transactions on Computational Science IV, vol.5430, pp.1-22, 2009.
URL : https://hal.archives-ouvertes.fr/lirmm-00372052

R. Merkle, Method of providing digital signatures, 1982.

M. Blum, W. Evans, P. Gemmell, S. Kannan, and M. Naor, Checking the correctness of memories, Proceedings. 32nd Annual Symposium in Foundations of Computer Science, pp.90-99, 1991.

W. E. Hall and C. S. Jutla, Parallelizable authentication trees, Selected Areas in Cryptography, pp.95-109, 2006.

R. Elbaz, D. Champagne, R. B. Lee, L. Torres, G. Sassatelli et al., Tec-tree : A low-cost, parallelizable tree for efficient defense against memory replay attacks, Cryptographic Hardware and Embedded Systems -CHES'07, pp.289-302, 2007.
URL : https://hal.archives-ouvertes.fr/lirmm-00179776

R. M. Best, Microprocessor for executing enciphered programs, vol.1979

, Preventing software piracy with crypto-microprocessors, IEEE Computer Society, pp.466-469, 1980.

, Crypto microprocessor for executing enciphered programs, 1981.

, Crypto microprocessor that executes enciphered programs, 1984.

, DS5002FP Secure Microprocessor Chip, Dallas Semiconductor, 2006.

D. Lie, C. Thekkath, M. Mitchell, P. Lincoln, D. Boneh et al., Architectural support for copy and tamper resistant software, Proceedings of the Ninth International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS IX, pp.168-177, 2000.

D. Lie, J. Mitchell, C. A. Trekkath, and M. Horowitz, Specifying and verifying hardware for tamper-resistant software, Proceedings of the 2003 IEEE Symposium on Security and Privacy (SP'03), pp.166-177, 2003.

D. Lie, C. A. Trekkath, and M. Horowitz, Implementing an untrusted operating system on trusted hardware, Proceedings of the 9th ACM Symposium on Operating Systems Principles (SOSP'03), pp.178-192, 2003.

J. Yang, Y. Gao, and L. Zhang, Fast secure processor for inhibiting software piracy and tampering, IEE Transactions on Computers. IEEE, pp.351-360, 2003.

, Improving memory encryption performance in secure processors, IEE Transactions on Computers. IEEE, pp.630-640, 2005.

G. E. Suh, D. Clarke, B. Gassend, M. Van-dijk, and S. Devadas, Aegis : Architecture for tamper-evident and tamper-resistant processing, Proceedings of the 17th International Conference on Supercomputing (ICS'03), pp.160-171, 2003.

, Efficient memory integrity verification and encryption for secure processors, Proceedings of the 36th Annual IEEE/ACM International Symposium on Microarchitecture, 2003.

D. Clarke, S. Devadas, M. Van-dijk, and B. Gassend, Incremental multiset hash functions and their application to memory integrity checking, Advances in CryptologyAsiaCrypt 2003 : 9th International Conference on the Theory and Application of Cryptology and Information Security, pp.188-207, 2003.

B. Gassend, G. E. Suh, D. Clarke, M. Van-dijk, and S. Devadas, Caches and hash trees for efficient memory integrity verification, Proceedings of the 9th International Symposium on High-Performance Computer Architecture (HPCA'03), pp.295-306, 2003.

G. Duc and R. Keryell, CryptoPage : an efficient secure architecture with memory encryption, integrity and information leakage protection, Proceedings of the 22th Annual Computer Security Applications Conference (ACSAC'06), pp.483-492, 2006.

G. Duc, Support matériel, logiciel et cryptographique pour une exécution sécurisée de processus, 2007.

W. Shi, H. S. Lee, C. Lu, and M. Ghosh, High speed memory centric protection on software execution using one-time-pad prediction, Georgia Institute of Technology, 2004.

, Architectural support for high speed protection of memory integrity and confidentiality in multiprocessor systems, IEEE, pp.123-134, 2004.

, Architectural support for high speed protection of memory integrity and confidentiality in multiprocessor systems, Special issue : Workshop on architectural support for security and anti-virus (WASSA'05), pp.6-15, 2005.

W. Shi, C. Lu, and H. S. Lee, Transactions on high-performance embedded architectures and compilers i, Centric Security Architecture, pp.95-115, 2007.

R. Elbaz, Hardware mechanisms for secured processor-memory transactions in embedded systems, 2006.
URL : https://hal.archives-ouvertes.fr/tel-00142209

R. Elbaz, L. Torres, G. Sassatelli, P. Guillemin, and M. Bardouillet, PE-ICE : Parallelized encryption and integrity checking engine, Proceedings of the 9th IEEE workshop on Design and Diagnostics of Electronic Circuits and Systems, pp.141-142, 2006.
DOI : 10.1109/ddecs.2006.1649595
URL : https://hal.archives-ouvertes.fr/lirmm-00102755

L. Su, Confidentialité et intégrité du bus mémoire, 2010.

L. Su, S. Courcambeck, P. Guillemin, C. Schwarz, and R. Pacalet, Secbus : Operating system controlled hierarchical page-based memory bus protection, Design Automation & Test in Europe, pp.570-573, 2009.

, Vsi alliance virtual component interface standard version 2 (ocb 2 2.0)

, EasyCrypt

G. Barthe, B. Grégoire, S. Heraud, and S. Z. Béguelin, Computer-aided security proofs for the working cryptographer, Advances in Cryptology -CRYPTO 2011, vol.6841, pp.71-90, 2011.
DOI : 10.1007/978-3-642-22792-9_5
URL : https://hal.archives-ouvertes.fr/hal-01112075