Proven Embedded WebAssembly runtime in SPARK
AdaCore
Paris
Internship
AdaCore: Helping Developers Build Software that Matters
Everything we do at AdaCore is centered around helping developers build safe, secure and reliable software.
For over 25 years, we've worked with global leaders across the military and civil avionics, defense systems, air traffic management/control, space, railway, and financial services industries, building tools and providing services that ease the complex and difficult process of developing high-integrity software. As the need for truly secure and reliable applications expands into industries such as automotive, medical, energy, and IOT, we’re advancing our time-tested technologies to bring expertise and services to help a whole new generation of developers. Through our subscription-based business model and dedicated services arm, we have worked with hundreds of customers over the year on thousands of projects.
Our 150 experts worldwide in the US (New York), France (Paris, Toulouse, Grenoble and Vannes), Germany, the UK, and Estonia, all play a role in developing state-of-the-art technologies to meet the challenges of building the highest grade of software.
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:
WebAssembly (a.k.a.WASM) is relatively new technology that enables the use of compiled languages such as C/C++, Rust, Ada, and others as alternatives for JavaScript in web development, but not only. Lightweight embedded WASM run-times can bring portability and security features for edge computing, micro-services, smart contracts applications, etc.
The sandboxed nature of WASM is an important property for security. However, for this property to hold the runtime must be free of defects and vulnerabilities. At the same time, the correctness of WASM instruction decoding and interpretation is absolutely essential for its trustworthiness.
The goal of this internship is to explore the use of formal verification in the implementation of an embedded WASM run-time. Using AdaCore’s industry ready formal verification solution called SPARK, you will implement a minimal WASM interpreter and prove the absence of vulnerabilities. In a second phase, you will push the proof to include functional correctness of the WASM execution.
Goals:
-
Get a first understanding of the WebAssembly technology
-
Get a first understanding of the SPARK technology
-
Implement a first minimal version of a WASM runtime
-
Adapt the first implementation for formal verification
-
Push the formal verification into functional correctness
-
Write a blog post to communicate the effort to the WASM and SPARK communities
-
Possible extensions to this list could include performance comparison with existing WASM runtimes, and optimisation
Skills required or Nice to have:
-
Interest for low-level/system programming
-
Interest for formal verification
-
Knowledge of WebAssembly (nice to have)
-
Knowledge of CPU emulation and or virtual-machines (nice to have)
-
Curiosity and interest for technical innovation
-
Will and ability to work autonomously
Timeframe & Location:
- During 2024 – 6 months
- Paris, France
Beyond the job
We are looking for individuals who want their work to have a direct impact on improving the reliability, safety and security of the software that modern society has grown increasingly dependent on in an international environment. Our sales and marketing team is staffed with multi-talented, tenacious and creative individuals; and our HR team is committed to ensuring your tenure with AdaCore is a positive one.
AdaCore is a global organization driven by a team that personifies many different backgrounds and experiences. We are also a technology company that celebrates the open exchange of ideas, which makes innovation possible! We encourage applicants of all backgrounds to consider joining us. We welcome people of all ethnicities, nationalities, gender identities or expressions, ages, religions, physical abilities, sexual orientations, veteran status, or marital status; we celebrate everything that makes you uniquely, undeniably you.
We encourage our employees to explore their curiosity by providing them ongoing and lifelong training from their first day in AdaCore with a strong onboarding plan. As we know that juggling work and life is challenging, we offer flexibility to accommodate personal needs and work commitments.
AdaCore offers competitive compensation, benefits and thoughtful perks (summer meetings, activity weekends, Holiday dinner etc). We go beyond industry standards to help keep our employees comfortable and satisfied both on and off the job, no matter where they are based.