Ph.D.: Assisting the design of secured applications for mobile vehicles
Supervisor: Ludovic Apvrille, Renaud Pacalet, sophie Coudert, Département Communications et Electronique TELECOM ParisTech 2229 routes des Crêtes – BP 193 F-06904 Sophia-Antipolis Cedex Téléphone : (33) 4 93 00 84 06 Fax : (33) 4 93 00 82 00
Email : Ludovic Apvrille and Sophie Coudert
Scientific context
Embedded system design methodologies are one important research topic of the LabSoC team. More particularly, the team focuses on methodologies that offer strong guarantees in terms of security requirement. An example of requirements to satisfy is resisting to attacks on communication protocols or on functions implemented by the system under design. Note that those protocols and functions may be implemented using a mix of hardware and software sub-functions. Work to be performed in that thesis is part of a European project starting in 2008, and focusing on the security of systems embedded into vehicles. For those systems, security requirements typically concern the resistance to attacks on communications between a vehicle and its surrounding infrastructures, and also on communications between vehicles.
Common techniques used to developed such secured systems are based on methodological cycles including (1) a requirement capture phase, (2) a modeling and proof phase: candidate hardware and software functions are proved to resist to listed security requirements, (3) an implementation phase: the system is implemented according to the modeling done in previous phase, and then (4) a test phase: the implemented system is proved to really resist to previously analyzed security threats. Unfortunately, the link between proofs performed on the system modeling, and the concrete implementation of the system is commonly not formal. That is, resistance to security threats made at modeling stage are only applicable to the modeled system – i.e. at a quite high level of abstraction - , and not on the final application. Even if testing techniques are used on that final application, tests lead are not exhaustive and are generally complex and long to apply. Moreover, the increasing complexity of embedded systems emphasizes this testing issue.
One possible solution to that issue relies on formal environments offering a way to preserve proved properties from the highest level of abstraction until the implementation level. For example, the B method integrates a formal refinement process based on property preserving from one level of abstraction to another more refined level. Unfortunately, we do think these approaches are not suitable for our application. Indeed:
- We do not wish to deeply modify usual methodologies for designing secured embedded applications.
- Techniques similar to the B-method, combined to the very high complexity of embedded systems mentioned above would probably lead to complex proofs i.e. to frequent and complex interactions between the person in charge of the modeling and proofs, and the proof engine itself. In our approach, we would like to leverage, as far as possible, those kinds of proof interactions.
Contributions
An interesting approach to experiment is based on tightly coupled automatic code generation and formal proofs techniques:
- The application is modeled, and requirements are proved to be satisfied over that application. Since the modeling of the application is quite abstract, only a code skeleton may be automatically generated. At this step, we wish to guarantee that this code skeleton preserves properties previously proved as satisfied. Note that this code skeleton is meant to be executed on an operating system and on a given hardware platform i.e. proof preservation must take into account all underlying software and hardware layers.
- Then, the automatically generated code is enriched until the final application. To preserve previously proved properties, allowed code modifications will have to be closely defined, while letting enough modification possibilities to persons in charge of the code. More precisely, allowed code modifications shall take into account usual embedded systems functions, to allow an “easy” coding of the latter.
Finally, the thesis work includes:
- The definition of a modeling and formal proof environment able to take into account systems embedded into vehicles and security constraints requirements. That environment may be based on previous work, e.g. the UML TURTLE profile [1].
- The definition of a code generator taking as input an application modeling and preserving prelisted security-related properties. This work is quite innovative but it may be based on automatic code generation techniques used to preserve other kinds of properties e.g. liveness properties.
- The definition of a methodology preserving security-related properties, and offering generated code enrichments. Once again, that part is quite innovative, and may be settled on nowadays testing and refinement techniques.
- The definition of a framework that integrates all techniques mentioned above. The TTool UML toolkit [2] might be a good candidate for this.
- At last, all contributions shall be evaluated over vehicle-based embedded systems. That evaluation will be lead with other international academic and industrial partners.
Skills
- Software-engineering / computer-engineering (compulsory)
- Modeling techniques (e.g. UML)
- Formal description techniques
- Wish to tackle embedded systems i.e. both hardware and software parts
- Security (protocols, cryptography, and so on)
References
[1] L. Apvrille, J.-P. Courtiat, C. Lohr, and P. De Saqui-Sannes. “TURTLE: A Real- Time UML Profile Supported by a Formal Validation Toolkit”. In IEEE transactions on Software Engineering, volume 30, pages 473-487, Jul 2004.
[2] TTool. The TURTLE Toolkit. In http://labsoc.comelec.enst.fr/turtle/ttool.html.
To candidate to that thesis, please send an e-mail to Ludovic Apvrille and Sophie Coudert. That e-mail should include a covering letter, a CV, master's grades and ranking, and recommendation letters. Incomplete files will not be considered