Ada
SPARKNaCl: A Verified, Fast Re-implementation of TweetNaCl
<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.
Weitere Infos
| Format | devroom |
|---|
Weitere Sessions
| 06.02.22 |
<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 ...
|
| 06.02.22 |
<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 ...
|
| 06.02.22 |
<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>
|
| 06.02.22 |
<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>
|
| 06.02.22 |
<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> ...
|
| 06.02.22 |
<p>SweetAda is a lightweight development framework whose purpose is the implementation of Ada-based software systems.</p>
|
| 06.02.22 |
<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 ...
|
