Conception Assistée des Logiciels Sécurisés pour les Systèmes Embarqués

A vast majority of distributed embedded systems is concerned by security risks. The fact that applications may result poorly protected is partially due to methodological lacks in the engineering development process. More specifically, methodologies targeting formal verification may lack support to certain phases of the development process. Particularly, system modeling frameworks may be complex-to-use or not address security at all. Along with that, testing is not usually addressed by verification methodologies since formal verification and testing are considered as exclusive stages. Nevertheless, we believe that platform testing can be applied to ensure that properties formally verified in a model are truly endowed to the real system. Our contribution is made in the scope of a model-driven based methodology that, in particular, targets secure-by-design embedded systems. The methodology is an iterative process that pursues coverage of several engineering development phases and that relies upon existing security analysis techniques. Still in evolution, the methodology is mainly defined via a high level SysML profile named Avatar. The contribution specifically consists on extending Avatar so as to model security concerns and in formally defining a model transformation towards a verification framework. This contribution allows to conduct proofs on authenticity and confidentiality. We illustrate how a cryptographic protocol is partially secured by applying several methodology stages. In addition, it is described how Security Testing was conducted on an embedded prototype platform within the scope of an automotive project.Une vaste majorité de systèmes embarqués distribués sont concernés par des risques de sécurité. Le fait que les applications peuvent être mal protégées est partiellement à cause des manques méthodologiques dans le processus d’ingénierie de développement. Particulièrement, les méthodologies qui ciblent la vérification formelle peuvent manquer de support pour certaines étapes du processus de développement SW. Notamment, les cadres de modélisation peuvent être complexes à utiliser ou ne pas adresser la sécurité du tout. Avec cela, l’étape de tests n’est pas normalement abordée par les méthodologies de vérification formelle. Néanmoins, nous croyons que faire des tests sur la plateforme peut aider à assurer que les propriétés vérifiées dans le modèle sont véritablement préservées par le système embarqué. Notre contribution est faite dans le cadre d’une méthodologie nommée Avatar qui est basée sur les modèles et vise la sécurité dès la conception du système. La méthodologie est un processus itératif qui poursuit la couverture de plusieurs étapes du développement SW et qui s’appuie sur plusieurs techniques d’analyse de sécurité. La méthodologie compte avec un cadre de modélisation SysML. Notre contribution consiste notamment à étendre le cadre de modélisation Avatar afin d’aborder les aspects de sécurité et aussi à définir une transformation du modèle Avatar vers un cadre de vérification formel. Cette contribution permet d’effectuer preuves d’authenticité et confidentialité. Nous montrons comment un protocole cryptographique est partiellement sécurisé. Aussi, il est décrit comment les tests de sécurité ont été menés sur un prototype dans le cadre d’un projet véhiculaire