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.
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 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).
It'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.
> - behavior for arbitrary sizes, such as integer overflows for large sizes
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).
> they are using unsigned 64-bit values (which conveniently have defined overflow semantics) for the lengths of the input buffer.
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.
Would you drive (aka 'use') a robotic car without a roll cage, safety belts, crumple zones and air bags because its software is proven correct? I would not.
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.
Why would that be obvious? It would require way more work to prove, but I think I could define a set of rules about the world and a control mechanism for an autonomous vehicle that guaranteed there would never be a collision at dangerous speed (Getting that work at reasonable speed and with enough 9s of availability to make the thing practical will be even more work)
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 scale difference is the difference between trivial and serious. Cosmic rays aren't nearly as much a hazard of day-to-day programming as other cars are of day-to-day driving.
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: