Security Levels for Initialised Memory Sections

[l-kent]

Currently the security level of the initialised memory sections put in the precondition of main() are not specified. We should assume them to be low for now, and either add axioms for them or add this information to the precondition of main(). We should also make care to exclude any global variables in the .data section from this assumption, as the security levels of those should be specified by the user.

Whether to use axioms or put this information in the precondition of main relates to #81 - it would only really be safe to add axioms for them if they are never written to by the program.

The axioms would look like axiom gamma_load8(mem, _address_); for each byte of the initialised memory that we want to specify as low.

Future work would include a way for the user to manually specify security levels for other parts of the initial memory, but that isn't relevant for now and should wait until a wider rework of the specifications has taken place.

[l-kent]

Since Boogie doesn't support axioms referencing mutable global variables (I forgot), it would make sense to instead insert these as free requires/ensures clauses for every procedure, similar to the approach taken in #92.

The most relevant examples are arrays_simple/gcc and arrays_simple/gcc_pic, but these pose an additional problem - the address of the stack_chk_guard symbol isn't currently initialised at all (because it can't be), so we probably want to additionally make the offsets in .rela.dyn of type R_AARCH64_GLOB_DAT return values that are low, as well as the memory sections we already initialise from #92.