Improve SPARK Capabilities for the Generation of Exploits

AdaCore: Helping Developers Build Software that Matters

Everything we do at AdaCore is centered around helping developers build safe, secure and reliable software.

For 30 years, we've partnered with global leaders in aerospace & defense, air traffic management, space, railway and financial services. We've developed tools and services simplifying high-integrity software development through a subscription-based model. As demand for secure applications grows in industries like automotive, medical, energy, and IoT, we're adapting our proven technologies to assist a new generation of developers.

Our 150 global experts based in the US, France, Germany, the UK, and Estonia, collectively develop cutting-edge technologies to address the challenges of high-grade software development.

Joining AdaCore is about joining a culture of innovation, openness, collaboration and dependability, which defines how we work together, with our customers and partners.

Context

SPARK is a subset of the Ada programming language, together with formal verification tools which allow giving mathematical guarantees about SPARK programs, from correct data flows to absence of runtime errors to correct implementation of functional requirements. SPARK is open source and freely available to the Community on Alire, a package manager for Ada, as well as professionally supported by AdaCore, which co-develops SPARK with Inria.

Goals

When the SPARK tool is unable to verify a program, it can sometimes generate exploits or counterexamples. It is a set of concrete values which can help the user understand how to trigger a defect in the program (a buffer overflow, a division by zero etc). This capability is very useful for users, as SPARK messages can be difficult to understand, especially for beginners.

The goal of the internship is to extend this capability to generate exploits on more programs. This would include extending both the fuzzer which generates random values, and the SPARK interpreter used to verify the candidate counterexample values.

A new capability to generate an executable testcase that exhibits the new generation of exploits could be implemented in the SPARK tool.

Skills required/nice to have:

• good understanding of program semantics and good programming skills
• an interest in formal methods
• experience with proof tools is a plus

Timeframe & Location:

During 2025 - 6 months - Toulouse office

Beyond the job

We're a global organization driven by diverse backgrounds, fostering innovation through an open exchange of ideas. We welcome applicants of all backgrounds, celebrating diversity in ethnicity, nationality, gender, age, religion, abilities, sexual orientation, veteran or marital status. 

Our commitment is to help our teammates, wherever they are based, feel comfortable and satisfied, by encouraging flexibility to ensure them a healthy work-life balance. Additionally, we prioritize individual development by offering continuous training from day one with a personalized onboarding plan.