In Ada95, the Unbounded_String type is often more flexible than the
String type because it is automatically resized as necessary.
However, don't store especially sensitive secret values such as passwords
or secret keys in an Unbounded_String, since core dumps and page areas
might still hold them later.
Instead, use the String type for this data, lock it into memory
while it's used, and overwrite the data as
soon as possible with some constant value such as (others => ' ').
Use the Ada pragma Inspection_Point on the object holding the secret
after erasing the memory.
That way, you can be certain that
the object containing the secret will really be erased
(and that the the overwriting won't be optimized away).
It's common for beginning Ada programmers to believe that the
String type's first index value is always 1, but this isn't true if
the string is sliced.
Avoid this error.
It's worth noting that SPARK is
a ``high-integrity subset of the Ada programming language'';
SPARK users use a tool called the ``SPARK Examiner'' to check
conformance to SPARK rules, including flow analysis, and there are
various supports for full formal proof of the code if desired.
See the SPARK website for more
To my knowledge, there are no OSS/FS SPARK tools.
If you're storing passwords and private keys you should still
lock them into memory if appropriate
and overwrite them as soon as possible.
Note that SPARK is often used in environments where paging does not occur.