E.g., a password that should be erased from memory, not just freed; a file that should be shredded, not just deleted.
This issue isn't about providing the ability to erase from memory or disk; rather, it's about marking certain values in code as having the characteristic of needing to be erased. A variable that holds a password or a CC num or similar would be a good example. By marking such a variable as sensitive, a programmer could force the intent compiler to prove that as soon as it receives its last use, a shred/delete function is called. It could also be used to prove that no sensitive values are written in plain text to a GUI (as in password entry boxes) or to a log file.
Might also want to use this mark to force in-memory encryption of sensitive data, so a crash dump doesn't expose it. And also locking sensitive data so it can't be paged to disk.
E.g., a password that should be erased from memory, not just freed; a file that should be shredded, not just deleted.
This issue isn't about providing the ability to erase from memory or disk; rather, it's about marking certain values in code as having the characteristic of needing to be erased. A variable that holds a password or a CC num or similar would be a good example. By marking such a variable as sensitive, a programmer could force the intent compiler to prove that as soon as it receives its last use, a shred/delete function is called. It could also be used to prove that no sensitive values are written in plain text to a GUI (as in password entry boxes) or to a log file.
Might also want to use this mark to force in-memory encryption of sensitive data, so a crash dump doesn't expose it. And also locking sensitive data so it can't be paged to disk.