heisenbugltd / saatana Goto Github PK

Apparently the (unused and private) Lemmas child package is ignored by gnatprove ATM. Probably, because the package is not in any closure of a main subprogram.

Heaving recently fixed all the coding standards violations (unnamed block statements etc.) I figured that a gnat check run should be done automatically, either as part of the build process or even a commit trigger.

After these declarations in saatana-crypto.ads we should do something like:

pragma Assert (for all W in Word_32'Range =>
                 To_Unsigned (To_Stream (W)) = W);
   --  Prove bijectivity of conversion subprograms.

We cannot do this directly in Saatana.Crypto:

non-static call not allowed in preelaborated unit

as the package is supposed to be Pure and shall remain so.

An idea might be to introduce private proof property child packages for the specific purpose of proving such kind of properties.

If we're running the prover on the CI runs, we could upload the prove results for further analysis.

Right now there are some "might not be initialized" warnings which should be investigated. Most likely cause is that we run a different set of provers than on my local machine (where Z3 and CVC4 are also installed).

• *.cwsi should have been *.cswi
• *.stdout not recognized, probably because the separating semicolon is considered part of the pattern

Sent from my Moto G (5) Plus using FastHub

Proof takes quite some time, especially if this project ever gets larger, so it seems impractical to run the full proof at each repository push.

Instead, we could just do a build (including running the KAT(s)), and do a proof run once or twice a day.

The currently used provers can prove all assertions which have been added prior to calling De/Encrypt_Bytes, yet for some unexplained reason, the actual precondition can not be proven by the tools.

This issue is a placeholder for manual triggers of proof runs.

If you add the special 'run_proof' label, a proof run on the master branch should be triggered.

As pointed out by Piotr Trojanek in the SPARK discussion mailing list, the Assume pragmas were wrong and not correctly catering for the fact that an empty input array with rather "interesting" bound could be passed to Encrypt/Decrypt_Bytes and Process_AAD, This is a rather serious bug as it would have opened the door to a DoS attack on the implementation if runtime checks were enabled.

The prover was right, after all.

We should upload the full results of the Known Answers Test run. These are important artifacts supporting our proof of functional correctness.

We should include a performance test, preferably with different optimization options and a comparison between run-time checks enabled and disabled (as we prove there will be none).

Candidates:

Block Ciphers:

• Blowfish
• Twofish
• Threefish, this one is based on Skein, so the SPARKSkein implementation would be a good start
• AES (PDF)
• IDEA (the patent expired in 2012, so it should be free to use now, but proper documentation seems scarce)

Stream ciphers:

• HC-256 (PDF)
• ISAAC
• Serpent

And then there's the thing that any proper encryption needs a cryptographically secure random number generator, be it for nonce, key, or random seed initializations.

The post condition on Crypto.Phelix.H isn't very readable, this should be improved.

It would be nice to have it expressed in a form that side-by-side comparison with the algorithm specification would be possible.

It looks as if the provers now report the "might not be initialized" messages at different places for where we do partial assignments. This should get fixed.

Latest SPARK CE Release seems to have the new aspect Relaxed_Initialization, which should help in proving most of the data initialization which currently is manually justified, see SPARKNaCl.

This requires updating the docker images to GNAT CE 2020.