Session
Schedule FOSDEM 2022
Ada

SPARKNaCl: A Verified, Fast Re-implementation of TweetNaCl

D.ada
Roderick Chapman
<p>SPARKNaCl is a new, verified and fast reefrence implementation of the NaCl API, based on the TweetNaCl distribution. It has a fully automated, complete and sound proof of type-safety and several key correctness properties. In addition, the code is fast - out-performing TweetNaCl on an Ed25519 Sign operation by a factor of 3 at all optimization levels. This talk will cover how "Proof Driven Optimization" can result in code that is both correct and fast on bare-metal embedded targets.</p>
TweetNaCl is a compact reference implementation of the NaCl API. It was initially constructed to show that an entire crypto library could fit into "100 tweets", but has since been re-used in some critical applications, such as the WireGuard VPN. There are no comments in the code at all, and all assurance rests on a single brief academic paper, and the formidable reputation of the authors. Can we do better? Can we produce a reference implementation which is amenable to automatic verification and yet is competitive with TweetNaCl in terms of performance and code size? This talk presents SPARKNaCl - a complete re-implementation of TweetNaCl in SPARK, which comes with a fully automated proof of type-safety, memory-safety and a number of key correctness properties. Having established a solid foundation, we went on to compare the performance and code size of SPARKNaCl against the original C implementation. Various transformations and optimizations have been applied that result in SPARKNaCl out-performing TweetNaCl on a bare-metal 32-bit RISC-V machine for a single Ed25519 "Sign" operation, while retaining automation and completeness of the proof. Furthermore, SPARKNaCl is freely available under the 3-clause BSD licence. This talk will present an overview of the results from both the proof work and performance analysis of SPARKNaCl.

Additional information

Type devroom

More sessions

2/6/22
Ada
Fernando Oleo Blanco
D.ada
<p>Welcome to the Ada Developer Room at FOSDEM 2020, which is organized in cooperation with Ada-Europe and Ada-Belgium.</p> <p>This year marks the first edition on which the devroom takes place on an online format. For that reason, this presentation will explain how does it work and how can the public use the systems provided by FOSDEM and interact with the speakers. We will also introduce the Ada-Europe and Ada-Belgium organisations. This small introduction also serves as a test to make sure ...
2/6/22
Ada
Jean-Pierre Rosen
D.ada
<p>An overview of the main features of the Ada language, with special emphasis on those features that make it especially attractive for free software development.</p> <p>Ada is a feature-rich language, but what really makes Ada stand-out is that the features are nicely integrated towards serving the goals of software engineering. If you prefer to spend your time on designing elegant solutions rather than on low-level debugging, if you think that software should not fail, if you like to build ...
2/6/22
Ada
Stefan Hild
D.ada
<p>In 2020 I started live streaming the development of a turn-based strategy game. At that time I had little idea about Ada, programming or game development (nothing has changed about that to this day). But by September 2020 it had taken the early form of a Civilization clone. After more than a year of development, it has become almost a real game with its own features. And now I'm going to talk a little bit about some experiences and weirdnesses with game development in Ada</p>
2/6/22
Ada
Jean-Pierre Rosen
D.ada
<p>The requirements for Ada numerics were to provide portable arithmetics without unacceptable performance cost. This talk shows how this was achieved by interval arithmetics without requiring a particular implementation model, like IEEE arithmetics.</p>
2/6/22
Ada
D.ada
<p>At FOSDEM 2020 we presented the first version of Alire, the package manager for the Ada Open Source ecosystem. Two years later, the tools and its ecosystem have evolved, in some instances based on the feedback received at FOSDEM. So we want to give you an update on the new features and improvements, including:</p> <ul> <li>Pin system: intended to help with the development and use of WIP crates.</li> <li>Crate configuration: that enables static code generation before compilation.</li> ...
2/6/22
Ada
Gabriele Galeotti
D.ada
<p>SweetAda is a lightweight development framework whose purpose is the implementation of Ada-based software systems.</p>
2/6/22
Ada
Alejandro R. Mosteo
D.ada
<p>Ada 2022 is around the corner with many goodies in the form of new features and featurettes. Arguably small syntax sugar additions combine for the programmer's comfort, like for example user-defined literals and container aggregates, that allow natural initialization of user-defined containers with the same expressions used for basic arrays since the beginnings of Ada. In this talk, I discuss how these features allow the initialization of a container data type for heterogeneous values (a-la ...