Prevent Valid_Message without Verify_Message

[senier]

When building the IP sniffer test, I forgot to run Verify_Message before checking Structural_Valid_Message. While this was not a correctness issue (the context of cause was invalid), it took me some time to realize that. I wonder if we should add a predicate to those convenience operations that work on a whole message that states/requires that a verification has been attempted on a context. This way we could spot such oversights during proof.

[treiher]

We should make sure that such a predicate also works with Verify, not only with Verify_Message. I think the simplest solution would be to let the Initialize procedure add a predicate Unchanged to the context, which is automatically removed by any procedure with an in-out context parameter (i.e. Verify, Verify_Message, Take_Buffer, Switch and Update). All validation functions would then need a not Unchanged as precondition.

[senier]

Suggested name for the predicate: No_Verification_Attempted

[treiher]

The envisioned solution is not applicable, as the value of the predicate is unknown after a procedure with an in-out parameter. After some discussion we think there is no simple solution, which has no drawbacks.

A good solution is able to statically analyze, if the code could lead to a valid message before Valid_Message is called. The following properties should be fulfilled, before Valid_Message can be used:

• a complete verification (Verify_Message) or a incremental verification (Verify ) was performed
• at least a subset of all fields, which form a potential valid message, have been verified
• Verify have been called in the correct order
• if Verify is used in a nested way (see code example below), the correct condition checks have been done

Initialize (C, Buffer);

Verify (C, Field_A);
if Valid (C, Field_A) then
   Verify (C, Field_B);
   if Valid (C, Field_B) then
      ...
   end if;
end if;

For a good usability it should be possible to call Valid_Message (C) after this nested if-statements (if a correct incremental verification was done before). But I guess the verification tools would be only able to show the correct usage if Valid_Message is used inside of the nested if-statements.

[treiher]

After further discussion we came to the following idea as solution:

• Ensure that Verify is always called in correct order by predicate and appropriate pre- and postconditions
• Add precondition to Valid_Message that Verify of at least one potential final field is called (the postcondition of Verify_Message is extended accordingly)

This covers the first three aspects mentioned in the comment above. As field conditions are checked internally by Verify, it is not necessary to enforce the user to do same again. Calling Valid_Message after nested if-statements will be not possible in the way shown above (a workaround would be to bind the proof-state to a boolean value in a branch where the necessary verifications have been done - that value has to be checked before using Valid_Message).

The implementation comprises the following tasks:

• Add predicate Verification_Attempted (Context, Field)
• Add precondition to Verify (Context, Field), which enforces the validity of Verification_Attempted (Context, Field) for all definite predecessors of a Field
• Add a corresponding postcondition to Verify
• Add postcondition to Verify_Message and correspondig precondition to Valid_Message, which enforces the validity of Verification_Attempted for at least one potential final field
• Add postcondition, which preserves validity of Verification_Attempted, to all other procedures, which modify Context
• (Simplify Valid_Message to only check validity of potential final field and corresponding outgoing condition)