Lumos Maxima

This is the repository of the Lumos Maxima team participating to the VerifyThis 2020 Collaborative Long-term Verification Challenge

IMPORTANT: Please note that this project exists as part of a blog entry, article, or other similar material by AdaCore. It is provided for convenient access to the software described therein. As such, it is not updated regularly and may, over time, become inconsistent with the latest versions of any tools and libraries it utilizes (for example, the Ada Drivers Library).

Contacts:

Yannick Moy and Claude Marché

Participants:

Claude Marché, Sylvain Dailler, Johannes Kanig, Claire Dross, Yannick Moy

Webpage(s):

GitHub project

Description:

The repository contains a toy implementation in SPARK (a subset of the Ada programming language targeted at formal verification) of a key server, similar to HAGRID. We proved the following properties of the core functionality of the code:

• absence of runtime errors
• correct data and information flows
• functional correctness
• termination

Future Work (Not done yet)

• persistent data storage (currently the data is stored in memory)
• putting all info into the token instead of maintaining a map of tokens
• encrypting the token to avoid forging data
• absence of data races (might be out of scope for SPARK)

Collaborations:

We are interested in collaborating on the best approach to achieve the above goals, either with people willing to contribute to the project directly, or with people sharing the same overall goals with other languages and tools.

Resources:

If you want to know more about SPARK, please use these resources:

Interactive Website to learn Ada and SPARK

SPARK User's guide

SPARK source code