Formalizeren van ISA veiligheidseigenschappen aan de hand van Universele Contracten

Instruction Set Architectures (ISAs) worden vaak gespecificeerd in pseudocode, waardoor het onmogelijk is om eigenschappen erover te formaliseren. Het gebruik van een formele taal om de semantiek van ISAs te beschrijven, zoals Sail, maakt formele studie mogelijk. Een veelbelovende techniek om beveiligingseigenschappen van ISAs te specificeren, is universele contracten, die garanties uitdrukken van de machine en gelden voor alle programma's. Deze benadering is echter alleen nog maar gebruikt voor ISAs van capability machines, met amper tot geen bewijsautomatisatie en tot dusver heeft onderzoek zich gefocust op cut-down assembly talen. Het doel van dit voorstel is het ontwikkelen en automatiseren van de techniek van universele contracten voor het formaliseren van veiligheidsgaranties van ISAs. We zullen dit bereiken door Katamaran, een semi-automatische separation logic verifier voor Sail specificaties, te gebruiken en uit te breiden. Als eerste stap ligt de nadruk op theoretische ISAs met verschillende beveiligings features. Vervolgens zullen we de aanpak en de automatisering in Katamaran opschalen om grotere ISAs en complexere semantische features zoals concurrency en interrupts te kunnen verwerken, waarvoor generalisatie van universele contracten nodig is. Dit onderzoek brengt de universele contracten techniek toepasbaar voor meer algemene en realistische ISAs, zodat we uiteindelijk meer vertrouwen krijgen in de beveiliging van realistische processors en systemen.