Fast and formally verified C implementation of Base64
corp.galois.com
corp.galois.com
Let's be welcoming.
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.
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?
good and fast c code looks not like this.
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.
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).
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.
Actually, I don't see how they could have a bug of this nature unless the caller actually passed in invalid data. In the context in question, they have 64-bit pointers, and they are using unsigned 64-bit values (which conveniently have defined overflow semantics) for the lengths of the input buffer.
Even if the calculation for data_end overflows, that would mean one of two things: the caller improperly specified the buffer, or the memory model really does have a buffer whose addressing overflows. In the latter case, because they use an equality test and they have no check for magical address values (like say, NULL) of currbyte, I don't see how that'd be a bug in the implementation.
> - bugs when using particular functions of the API, such as base64_encode_update()
You mean bugs when using specific parts of the API in ways that are not consistent with their specification. It's hard to see why you'd even consider that a bug in the implementation. That's a bug in the caller.
> 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.
Are you sure about that? First, there doesn't appear to be much that would qualify as "internal state" to base64_encode_update(). The closest thing to internal state it has is base64_encodestate, which really only captures which of three states the state machine is in and a result code, both of which are provably in the correct state at the end of each invocation of the function.
I'm not clear as to why you think the proof doesn't cover base64_encode_update() being invoked multiple times. It's hard to know without understanding what their simulator does, but it sure looks and sounds like it is expanding the full set of possible execution paths through the b64enc, which would include up to N invocations of base64_encode_update(). The only way I can imagine it wouldn't be proving correctness for multiple base64_encode_update() calls is if the simulator always had fread() return ball all requested bytes AND you never proved it for cases where N > BUFSIZE (which would just be silly).
Yes, if you examine the code you can manually prove that it's safe: but that's not proven by their formal computer-checked proof.
As for the rest of your post: you seem to be assuming that what they proved is that b64enc.c behaves correctly. This is not true at all: they just proved that the helper function base64_encode() works correctly for a specific size (this is done in proof/sym_encode.c). This helper function never calls base64_encode_update() twice and is not used by b64enc.c, and that's why we don't know if the multiple-block implementation from b64enc.c actually behaves correctly.
You only need dynamic (run-time) checks to account for scenarios that the static (compile-time) checks couldn't rule out. For example, a Python programmer might use a run-time check to ensure a number is >= 0, but a C programmer can declare it as an unsigned int and not have to bother with that check.
In the same way, if we have a proof that, for all inputs, an index will never overflow an array, then we don't need a bounds check. Likewise for integer overflows, null pointers and any other assertion you like.
Proving a property holds for all inputs is more difficult than checking it holds for each input we are given, but the advantage is that in many situations a failed run-time check can be unrecoverable:
missile.nose.onImpact = function(event) {
switch (event.object) {
case target:
console.log('Hit!');
missile.explode();
break;
case silo.door:
// Should never get here...
console.log('Oops!');
break;
default:
console.log('Miss!');
break;
}
};
missile.fire();I think the way to go is to augment the model for what the function does with its behavior on erroneous inputs, and change to source code so that the prover can prove that the code implements the more robust model.
Problem is, the assumptions that such a model makes will be violated, either because the world is different than modeled or due to failure of a component. That is why you would want additional safety features.
That, IMO, is similar to the case where you build a component for base64 encoding, prove that it never will be called with a null pointer argument, and yet include that null pointer check and a way to signal errors in your component.
You can be sure "It will never happen" _will_ at some moment turn into "that's interesting", but you don't know where or when.
A straight up "no collisions" theorem would require proving limits on the behavior of other objects in and around the road and also that certain mechanical components never fail.
The 'only' difference is one of scale (orders of orders of magnitude.)
NULL checks for what? It's encoding binary, so there is no need to worry about NULL terminated strings. The only possible NULLs (the state pointer, the source pointer, or the target pointer).
Sure, you could make a version of the code that adds those checks, but particularly given the context of the problem, those checks would be superfluous. As an example, look the b64enc.c program and tell me how a NULL check would avoid a possible problem in the code.
> one endless loop based on pointer arithmetic
It's not an endless loop, and actually that's part of their formal proof. It ends when they reach the end of their input, which is provably true, even if your memory model allows a buffers allocation addresses overflow (e.g. a buffer that might start at 0xfe and finish at 0x10).
> good and fast c code looks not like this.
I'm not sure that you're a good judge of that. For example, the "endless loop" & switch statement that you refer to is actually a very standard approach to implementing a state machine in C. You'll find the moral equivalent of that code in a lot of parsers.
Minus the formal proof, this actually looks like very standard code with a lot of very common C idioms.
For example: GNU General Public License: http://www.gnu.org/licenses/gpl.html
Mentioned several times.
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*