Build a future of trust together

Thales is a global leader in high technologies specializing in three sectors: Defense & Security, Aeronautics & Space, and Cyber & Digital. It develops products and solutions that contribute to a safer, more environmentally friendly, and more inclusive world. The Group invests nearly 4 billion euros per year in Research & Development, particularly in key innovation areas such as AI, cybersecurity, quantum, cloud technologies, and 6G. Thales has nearly 81,000 employees in 68 countries.

Our commitments, your benefits

• Our technological know-how
• Our attention to employee balance
• An inclusive and benevolent environment
• Recognized societal and environmental commitment (Thales Solidarity, CAC 40 ESG index…)

Your daily life

The Gennevilliers Campus is the heart of design, development, and support activities for major defense systems: radio communications, resilient network and infrastructure systems, satellite communications, collaborative combat, and cybersecurity. Located north of Paris, it is quickly accessible by public transport.

The Cyberprotection Solution Engineering department conducts security engineering studies to protect its clients' (internal Thales) systems or products. This engineering takes various forms: security expertise, security architecture, specification engineering, and applies to objects of very diverse sizes: from security components to HW/SW products, up to systems, all for the purpose of protecting critical IT systems and communications. The department is heavily involved in security components.

In this context, members of this department participate in upstream research work concerning, among other things, the future of secure communications. This work takes the form of developing technological demonstrators to guide our reflections and support our recommendations.

Within this department, the AES security expertise laboratory seeks to improve its tools for auditing security projects. In this context, the intern will enrich the security expertise tools to test security products.

Your missions

The objective of the internship is to develop a data filter in Coq and to formally prove its correctness in Coq. It will involve proving that the filter correctly implements the filtering policy. The code will then be extracted to OCaml.

Coq is a language that allows both software development (a part of Coq is very close to OCaml), writing theorems, and writing proofs of these theorems.

By joining us, your main missions will include:

• training in Coq
• developing the software in Coq
• writing theorems formalizing the filtering policy
• proving these theorems

The supervisor is well-versed in Coq. You will therefore be able to acquire the necessary skills to work in the very promising field of formal methods applied to software security.

Your profile

You are currently pursuing a higher education degree (BAC+4/+5) specializing in Computer Science.

You have skills such as:

• An excellent level in mathematics, particularly in "mathematical logic."
• Scientific English
• First experience in functional programming (e.g., OCaml)

Do you recognize yourself? Then you have a good chance of thriving in our teams!

The team's word

This internship will be an opportunity for you to work in a team within an innovative company, to apply academic knowledge in an operational environment, and to develop new skills.

All our internships are conventioned and subject to gratification, the amount of which is determined according to your level of study.

Thales, a Handi-Engaged company, recognizes all talents. Diversity is our best asset. Apply and join us!