In dieser Masterarbeit sollen One-Instruction Set Computer (OISC) Architekturen, SUBLEQ und Varianten, daraufhin untersucht werden, unter welchen Voraussetzungen die Ausführung eines Programmes den Speicher invariant lässt. Hierzu können Methoden aus dem Bereich “Formal Proofs” und “Formal Verification” genutzt und angepasst werden. Die Ergebnisse sollen auf eine einfache statische Router oder Firewall Software angewandt werden (die vom Studierenden entwickelt wird) und gezeigt werden, dass Bereiche des Speichers nach dem routen/analysieren eines beliebigen Pakets sich nie verändern. Ziel soll es sein formal zu beweisen, dass unter bestimmten Bedingungen keine Speicher Korruption stattfinden kann.

Quellen:

[1] “Highly Automated Formal Proofs over Memory Usage of Assembly Code” - Freek Verbeek, Joshua A. Bockenek, Binoy Ravindran; 2020; TACAS
[2] “Formal Verification of Memory Preservation for x86-64 Assembly via Proof Generation” - Joshua A. Bockenek; 2019; Dissertation

Kontakt:

Michael Kissner (michael@akhetonics.com)