Implementation Guidelines

Data Sanitization

Data sanitization is an interesting issue. In a highly secure environment we'd like to guarantee that no traces of sensitive material are left lying around. The most useful approach would be based on Rod Chapman's blog post (PDF)

Unfortunately, at the time of writing this, the approach has several issues:

• limited types (by-reference semantic/no copying)

  Does not work with postconditions as 'Old cannot be used with limited types (using 'Old naturally implies copying).

• tagged types

  Does not work when applied directly to the whole Context type as the proof functions are seen as primitive operations and they cannot be declared after the full record declaration, yet they depend on the record type.

• Hybrid approach

  Include tagged components which should make the containing record a by-reference type. This at least solves the problem of guaranteeing by-reference semantics and does not pose a problems with proof functions. This is a bit more work than outlined in the above paper, but seems practical.

  Things to think about here: Derived data. For instance, the H function in the Crypto.Phelix component takes key material, which surely is sensitive, but these are simple 32-bit integers passed by copy.