Skip to content

Latest commit

 

History

History
46 lines (31 loc) · 1.79 KB

README.md

File metadata and controls

46 lines (31 loc) · 1.79 KB

verifythis-ltc-2020 Proof Status

This repository gathers the effort of the KeY team for the VerifyThis Collaborative Long-Term Challenge.

Project group:

  • Stijn de Gouw
  • Mattias Ulbrich (@matulbrich)
  • Alexander Weigl (@wadoon)

Note: The distributed key-2.7-exe.jar is licensed under GPLv2+. The license of the remaining Java sources are not determined yet.

Verified Software

A simply email-key map

In simplified/, you find a simple implementation for the keyserver -- verifiable without interactions in KeY. The implementation is based upon four integer arrays that store:

  • the id/email of the user, represented currently by an integer
  • two arrays for confirmed and unconfirmed keys, and
  • an array that stores confirmation codes.

The maximum number of users is fixed to 1024, as the arrays are never resized.

Map version

The next version builds upon the generalization of the previous map structure. It is currently work in progress. This is a two-step process. The first step is a provable version using maps of int to int. This avoids working with the heap.

  • KIMap (Key Integer Map) is an interface representing a map of Int -> Int. This functionality is bound to the behaviour of the map data type in KeY by JML specification.
  • KIMapImpl is a simple implementation based upon two int arrays, one for the key, the other the values.
  • KeyServerInt is a version of the backend of the verifying key server using integers as e-mail addresses and keys.

The second step is to use Strings. This results into KSMap and KSMapImpl and also the KeyServerString.