Security Engineering for Lifelong Evolvable Systems
Home

Gemalto

Gemalto (NASDAQ: GEMP) (Euronext NL 0000400653 GTO) is a leader in digital security with pro forma 2005 annual revenues of EUR1.7 billion ($2.2 billion), operations in 120 countries and 11,000 employees including 1,500 R&D engineers. The company's solutions make personal digital interactions secure and easy in a world where everything of value - from money to entertainment to identities - is increasingly represented as bits and bytes communicated over networks.

Gemalto thrives on creating and deploying secure platforms, portable and secure forms of software in highly personal objects like smart cards, SIMs, e-passports, readers and tokens. More than a billion people worldwide use the company's products and services for telecommunications, banking, e-government, identity management, multimedia content, digital rights management, IT security and other applications.

Gemalto R&D teams, which are located in France, Germany, Finland, US, Singapore and China, are involved in a lot of collaborative projects. In Europe, they participate to various research programs as IST, PIDEA, MEDEA+ and ITEA. Gemalto was formed in June 2006 by the combination of Axalto and Gemplus International S.A. The SecureChange project will involve people from our research centers  in Meudon and in La Ciotat, and in particular from the Formal Methods team and the case study developer team. Gemalto will use its knowledge in secure operating systems, applications, and software frameworks gained during years in the smart cards and terminal research domains. Our security people will use their expertise in Formal Methods, secure design and Common Criteria evaluations.

Gemalto, and in particular the Formal Methods team, has been involved into several European projects to investigate the improvement of the security of embedded software (FP6-Verifcard, Tool-assisted Specification and Verification of JavaCard Programs), INSPIRED (Integrated Secure Platform for Interactive Personal Devices), Medea (Onom@topic) and national projects EDEN2 (environment of tools for high level certification), POSE (model based testing of security policies). The team has been one of the contributors to the RESET project (Roadmaps for European research on Smartcard Technologies).

Key personnel:

Dr Boutheina Chetali: Head of the Formal Methods team, into the Security Labs of Gemalto's Technology and Innovation Department. Doctor in Computer Science, she has been working in the smart cards arena since 1999 when she joined the advanced research group of Bull Smart Card & terminals as R&D engineer expert in formal methods. Since 2001, she is in charge of the Formal Methods team (previously Schlumberger, Axalto) working on the application of formal methods to the security of the smart cards and to their Common Criteria certifications. Main activities of its group are the formalization of the Java card platform and its components, the verification of security properties, formal model-based testing and the Common Criteria evaluation at high levels (EAL5 to EAL7). She is also member of the Java Card Forum security group and the Global Platform security group. The main achievement of its group was the first smart card certificate using formal assurances from the EAL7 level, the highest Common Criteria certification level.

Dr Quang-Huy Nguyen: Research engineer in the Formal Methods and Security group of Gemalto since January 2003. Doctor in Computer Science, he works on the formal verification of the Java Card platform, the verification of security properties, and high level Common Criteria certification. He also works on the methods and processes for secure smart cards software development and evaluation.

Dr June Andronick: Research engineer in the Formal Methods and Security group of Gemalto since October 2002. Doctor in Computer Science, she works on the formal verification of embedded operating systems, using computer aided source code verification. She also works on the certification of the Java Card platform, the verification of security properties such as the confidentiality and the integrity and the model-based testing of security properties.