From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=unavailable autolearn_force=no version=3.4.4 X-Received: by 10.180.187.47 with SMTP id fp15mr914466wic.5.1373620263787; Fri, 12 Jul 2013 02:11:03 -0700 (PDT) Path: border1.nntp.dca3.giganews.com!border3.nntp.dca.giganews.com!border1.nntp.dca.giganews.com!nntp.giganews.com!cw2no15507706wib.0!news-out.google.com!md6ni56281wic.0!nntp.google.com!proxad.net!feeder1-2.proxad.net!137.226.231.214.MISMATCH!newsfeed.fsmpi.rwth-aachen.de!news-1.dfn.de!news.dfn.de!news.uni-weimar.de!medsec1.medien.uni-weimar.de!lucks From: Stefan.Lucks@uni-weimar.de Newsgroups: comp.lang.ada Subject: Re: The future of Spark . Spark 2014 : a wreckage Date: Fri, 12 Jul 2013 11:12:26 +0200 Organization: Bauhaus-Universitaet Weimar Message-ID: References: NNTP-Posting-Host: medsec1.medien.uni-weimar.de Mime-Version: 1.0 X-Trace: tigger.scc.uni-weimar.de 1373620264 3073 141.54.178.228 (12 Jul 2013 09:11:04 GMT) X-Complaints-To: news@tigger.scc.uni-weimar.de NNTP-Posting-Date: Fri, 12 Jul 2013 09:11:04 +0000 (UTC) X-X-Sender: lucks@debian In-Reply-To: User-Agent: Alpine 2.10 (DEB 1266 2009-07-14) Content-Type: TEXT/PLAIN; CHARSET=ISO-8859-15; FORMAT=flowed Content-Transfer-Encoding: QUOTED-PRINTABLE Content-ID: X-Original-Lines: 87 X-Original-Bytes: 4597 Xref: number.nntp.dca.giganews.com comp.lang.ada:182489 Date: 2013-07-12T11:12:26+02:00 List-Id: 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 j= unk > 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,=20 they usually take a lot less lines of "anno-code" than writing pre- and=20 postconditions. So even if you consider the data flow annotations as=20 redundant, their overhead is small. Thirdly, maybe my example has been too artificial. Below, I'll briefly=20 describe one real-world example. >> The fruits (well, bugs) you catch by employing pre- and postconditions a= re >> 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= =20 rid of that disease very very quickly. Turning naturally-written Ada into= =20 proper SPARK is a pain in the you-know-where!) One real life example (simplified for the purpose of posting this) is the= =20 implementation an authenticated encryption scheme. Consider two byte=20 strings X and Y of the same length, X being the message and being Y the=20 "key stream". There is additional authentication key K. The output of the= =20 authenticated encryption is the ciphertext (X xor Y), followed by a=20 cryptographic checksum(*) of X under the key K. Specifying and proving the first part of the output (X xor Y) was easy.=20 But specifying and proving the checksum part turned out to be tough. So I= =20 stopped trying it -- concentrating on the low-hanging fruits, as you put=20 it. However, I still had the flow annotations in my spec. (I use to write the= =20 flow annotations first, then the pre- and postconditions, and then the=20 implementation.) The flow annotations specified the flow from X and K to=20 Z. And that actually caught my error of using (X xor Y) instead of X in=20 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= =20 SPARK 05 provides, but I did find the work with old SPARK rather tedious,= =20 and I don't need that amount of assurance. ----------------- (*) The correct terminology would be "message authentication code" or=20 "MAC", rather than "checksum". ------ I love the taste of Cryptanalysis in the morning! ------ --Stefan.Lucks (at) uni-weimar.de, Bauhaus-Universit=E4t Weimar, Germany--