Promoting the use of formal methods for software security, in particular within
the context of small secure portable objects and ubiquitous computing, is the
main goal of the INRIA EVEREST research project.
By offering Globalplatform, world leader for the development and deployment
of secure smart card solutions, a formal model for the GlobalPlatform
Card Specification v2.1.1 specification, the research project provides
an IT solution designed to reinforce the security assessment of industrial
products, accelerate the process for compliance testing and facilitate
the development of subsequent versions of GlobalPlatform products. Boasting
57 members that include Visa and Mastercard International, IBM, Hitachi,
Thales, STMicroelectronics, Sun, Gemplus, etc., the representatives of
this consortium stress the added value of this type of model that provides
« a rigorous and unambiguous specification » for those
wishing to implement the v2.1.1.
Formal verification techniques will thus contribute to a deeper understanding
of complex security architectures that are widely used in the industry.
Emerging from fundamental research, it will also increase confidence in
the solutions implemented by encouraging adoption of the most pertinent
standards.
