20.500.12556/RUL-187782 Razvoj abstraktnega stroja s preverjanjem kode Development of an abstract machine with code verification Varno izvajanje programov zahteva strogo preverjanje kode, preden se program sploh izvede. Varnost lahko še dodatno okrepimo s sledenjem pretoku informacij, ki omogoča nadzor nad tem, kako se vrednosti prenašajo med različnimi deli sistema, predvsem standardnim vhodom in izhodom. V pričujočem delu je zasnovan eksperimentalni abstraktni stroj, katerega računski model združuje lastnosti skladovne in registrske arhitekture. Vrednosti na skladu so nespremenljive, nadzorni tok pa je omejen na pogojne stavke in klice funkcij. Stroj je implementiran kot knjižnica v jeziku Rust ter vsebuje izvajalnik za konkretno izvajanje programov in preverjalnik, ki pred izvajanjem opravi preverjanje kode z uporabo intervalov, ki predstavljajo možne vrednosti med izvajanjem. Oba dela stroja podpirata tudi sledenje pretoku informacij. Stroju je potrebno podati varnostno politiko, ki določa pravila za sledenje. Da se izognemo plazenju oznak, je s funkcijami za siromašenje mogoče spremeniti oznake podatkov iz strogih v ohlapne. Izdelani stroj uspešno preverja programe pred izvajanjem in izvaja sledenje pretoku informacij. Safe execution of programs requires strict code verification before the program is executed at all. Security can be further enhanced by information flow tracking, which allows control over how values are transferred between different parts of the system, especially standard input and output. In this thesis, an experimental abstract machine is designed, whose computational model combines properties of stack-based and register-based architectures. Stack values are immutable, and control flow is restricted to conditional statements and function calls. The machine is implemented as a library in the Rust language and includes an executor for concrete program execution and a verifier that performs code verification before execution using intervals that represent possible values during execution. Both parts of the machine also support information flow tracking. The machine requires a security policy that defines the rules for tracking. To avoid tag creep, it is possible to change data tags from strict to loose using downgraders. The developed machine successfully verifies programs before execution and performs information flow tracking. abstraktni stroj preverjanje kode enkratno prirejanje sledenje pretoku informacij abstract machine code verification single assignment information-flow tracking true false false Slovenski jezik Angleški jezik Diplomsko delo/naloga 2026-09-14 12:05:09 2026-09-14 12:05:14 2026-09-15 04:27:48 0000-00-00 00:00:00 2026 0 0 0000-00-00 NiDoloceno NiDoloceno NiDoloceno 0000-00-00 0000-00-00 0000-00-00 1970-01-01 38816 Pozenel_Matic_-_Razvoj_abstraktnega_stroja_s_preverjanjem_kode.pdf Pozenel_Matic_-_Razvoj_abstraktnega_stroja_s_preverjanjem_kode.pdf 1 E3AE0629BFE699B4C913C9A3DB1C0786 4c584e592f5ef413dc1c7bf94dc4e457160702b6d7c295ee241cc94103506ac5 bfc3264f-b023-11f1-8bc5-0050569b8976 https://repozitorij.uni-lj.si/Dokument.php?lang=slv&id=247533 Fakulteta za računalništvo in informatiko 0 0 0