Re: The future of Spark . Spark 2014 : a wreckage

[Stefan.Lucks@uni-weimar.de]

On Thu, 11 Jul 2013, Randy Brukardt wrote:

>> Who said, catch all bugs? I didn't.
>
> You want to catch this very unlikely bug, and add a giant pile of extra junk
> annotations for this purpose. My contention is that it won't catch enough
> bugs by itself to be worth the complication.

Firstly, whatever data flow annotations are, they are not "junk".

Secondly, there is no "giant pile" of data flow annotations. Actually, 
they usually take a lot less lines of "anno-code" than writing pre- and 
postconditions. So even if you consider the data flow annotations as 
redundant, their overhead is small.

Thirdly, maybe my example has been too artificial. Below, I'll briefly 
describe one real-world example.

>> The fruits (well, bugs) you catch by employing pre- and postconditions are
>> a bit higher, actually. At least, that is what I gather from my own
>> experience YMMV.
>
> Your experience seems to have been on annotating existing code,

Not at all! (Well, I tried once to SPARKify existing Ada code -- but I got 
rid of that disease very very quickly. Turning naturally-written Ada into 
proper SPARK is a pain in the you-know-where!)

One real life example (simplified for the purpose of posting this) is the 
implementation an authenticated encryption scheme. Consider two byte 
strings X and Y of the same length, X being the message and being Y the 
"key stream". There is additional authentication key K. The output of the 
authenticated encryption is the ciphertext (X xor Y), followed by a 
cryptographic checksum(*) of X under the key K.

Specifying and proving the first part of the output (X xor Y) was easy. 
But specifying and proving the checksum part turned out to be tough. So I 
stopped trying it -- concentrating on the low-hanging fruits, as you put 
it.

However, I still had the flow annotations in my spec. (I use to write the 
flow annotations first, then the pre- and postconditions, and then the 
implementation.) The flow annotations specified the flow from X and K to 
Z. And that actually caught my error of using (X xor Y) instead of X in 
the implementation.

>> Did you ever actually work with SPARK?
>
> No, there wasn't a free version when I was interested. And now that there is
> a free version, I'm no longer interested because it is too restricted to be
> useful in any of my code. And it tries to do too much as well.

Agreed! Well, certainly there are people who require as much assurance as 
SPARK 05 provides, but I did find the work with old SPARK rather tedious, 
and I don't need that amount of assurance.


-----------------
(*) The correct terminology would be "message authentication code" or 
"MAC", rather than "checksum".



------  I  love  the  taste  of  Cryptanalysis  in  the morning!  ------
     <http://www.uni-weimar.de/cms/medien/mediensicherheit/home.html>
--Stefan.Lucks (at) uni-weimar.de, Bauhaus-Universität Weimar, Germany--