10 ms·
Fast and formally verified C implementation of Base64
- eru 13y agoThe people at Galois do so many fascinating things. I recommend watching some of the talks they gave at each year's ICFP / CUFP. (Pick any, or all, if you have the talks.)
- afhof 13y ago"Beware of bugs in the above code; I have only proved it correct, not tried it."
- sigstoat 13y agospewing this quote with no context or further comment is just tedious FUD.
- eru 13y agoUnfortunately, yes. For those knowing the context, the comment is actually a compliment: comparing the authors with Knuth.
- jacquesm 13y agoIt serves as a reminder that even though this implementation has been proven correct that does not rule out bugs in the proof or in the method used to create the proof.
- gsnedders 13y agoOr that your compiler produces code equivalent to the (proven) correct C.
- derleth 13y agoThis was said by Donald Knuth, in case anyone here doesn't know that specific bit of trivia.
- Someone 13y agoFull story at http://staff.science.uva.nl/~peter/knuthnote.pdf http://staff.science.uva.nl/~peter/knuthnote.pdf. Does anybody know what the piece of typical Dutch furniture is?
- stingraycharles 13y agoI've read the article you've referenced but am unable to find the furniture you mention. At which page should I look?
- jacquesm 13y agoAt $10 my guess would be a milking stool.
- Someone 13y agoThat was my initial guess, too, but a) IMO, that is borderline furniture and b) it would surprise me if it were typically Dutch. Google gave me zillions of patents for milking stools (bucket attachments seem popular), but no definite answer to the latter question.
- jstanley 13y agoI like the Duff's device-like loop entry: https://github.com/davidlazar/base64/blob/master/base64encode.c#L35 https://github.com/davidlazar/base64/blob/master/base64encod...
- cbsmith 13y agoI wouldn't even really call that a duff's device like entry. It's a pretty standard implementation of a state machine... I'm still really scratching my head questioning to what extent you can really consider this implementation a "coroutine" solution. It sure looks to me like a state machine solution.
- rwmj 13y agoI particularly like how the C code is licensed "without a warranty": https://github.com/davidlazar/base64 https://github.com/davidlazar/base64
- deletes 13y agoAlmost every free or open source code has the line "without a warranty" somewhere in the agreement. For example: GNU General Public License: http://www.gnu.org/licenses/gpl.html http://www.gnu.org/licenses/gpl.html Mentioned several times.
- easytiger 13y agois this formally verified? I'm not sure whats going on but from a quick glance its just comparing the output of two implementations?
- panic 13y agoInstead of brute force, it looks like it's comparing automatically-generated models of the two implementations symbolically. Success! Amazingly, this proof systems scales to large values of n where exhaustive checking is not feasible: $ time make n=1000 Proving function equivalent to reference: encode_aig : [1000][8] -> [1336][8] Q.E.D. real: 17.882s user: 16.31s cpu: 1.50s*
- pjscott 13y agoModern SMT solvers are astonishingly fast for most real-world inputs. Not bad, considering that the problem they solve is NP-complete!
- dons 13y agoIt's doing symbolic equivalence checking via an SMT solver, iirc.
- deleted 13y ago[deleted]
- mbq 13y ago... from a company working for the NSA. (;
- waffenklang 13y agoGood example for the weaknesses of the 'formally verified' sale strategy. It may be formally correct, but the code is full of weaknesses, like no NULL checks, no out of bounds checks, one endless loop based on pointer arithmetic.. good and fast c code looks not like this.
- kd0amg 13y agono NULL checks, no out of bounds checks I would expect formal verification to make many instances of these superfluous. If this code genuinely needs to have these added, that sounds like a flaw in their verification system.
- waffenklang 13y agoI agree in the point that its the task of the fv-system to take care of this, and so its a flaw in it, if its necessary. imho,in this case it is a flaw, as the 'public' api function base64_encode wants the user to input pointer to 2 ptr to buffer with only for 1 given the length. and the code makes implicit assumption of the user input without checking it (encoded is manipulated).
- randomvisitor 13y agoIt's a flaw in the specification of the theorem, not in the verification. The way it works is that they choose fixed sizes INLEN and OUTLEN, and prove that when data points to a buffer of INLEN bytes, they can allocate a result buffer and base64_encode(data, INLEN, result) will compute the correct encoding. So, implied in this statement is the fact that the input buffer is valid (thus not null), and that the output buffer must be valid (and not null) and disjoint from the input buffer. There are more fundamental classes of bugs that this won't detect: - behavior for arbitrary sizes, such as integer overflows for large sizes - bugs when using particular functions of the API, such as base64_encode_update() The latter problem means that there is no proof that b64enc.c is correct at all, even for a fixed size: it's entirely possible that multiple calls to base64_encode_update() would corrupt the internal state.
- randomvisitor 13y agoIt's pretty impressive that this can be done completely automatically (model checking), although the price to pay is that he can only prove the implementation for a fixed input size. I'm very curious about what would happen if he dropped the safety check in base64_encode_value(). It would probably speed things up a little, but would the proof fail?
- cbsmith 13y agoYeah, I thought the safety check was rather curious really. It was also odd to use a NULL terminated string for the encoding set instead of a straight 64-byte array (sure, you only save 1 byte, and most compilers will no doubt waste that byte ANYWAY just for memory alignment reasons, but it still struck me as surprisingly... imprecise).