20.500.12556/RUL-175859 Formalizacija ločevalnega jedra z uporabo dokazovalnega pomočnika Formalization of a separation kernel using a proof assistant Med drugim lahko za zagotavljanje varnosti računalniškega sistema uporabimo ločevalno jedro. To je specializiran operacijski sistem, ki poskrbi za razdelitev virov sistema na ločene domene in za popolno ločitev med njimi. V tem magistrskem delu formaliziramo model ločevalnega jedra z uporabo dokazovalnega pomočnika. Najprej izberemo dokazovalni pomočnik. Izbirni postopek vključuje teoretični pregled nekaterih najpogosteje uporabljenih dokazovalnih pomočnikov in izvedbo poskusa v jezikih Rocq in Isabelle. Rezultate ovrednotimo in izberemo dokazovalni pomočnik Rocq za formalizacijo ločevalnega jedra. Formalizacija vključuje specifikacijo lastnosti jedra, specifikacijo varnostnih lastnosti in dokazovanje teh varnostnih lastnosti za definirano jedro. S tem postopkom zagotovimo pravilno delovanje jedra Among other things, a separation kernel can be used to ensure the security of a computer system. This is a specialized operating system that ensures the division of system resources into separate domains and complete separation between them. In this master’s thesis, we formalize a separation kernel model using a proof assistant. First, we select a proof assistant. The selection process includes a theoretical review of some of the most commonly used proof assistants and the implementation of an experiment in the Rocq and Isabelle languages. The results are evaluated and Rocq is selected for the formalization of the separation kernel. The formalization includes the specification of kernel properties, the specification of security properties, and the proof of these security properties for the defined kernel. This procedure ensures the correct function of the kernel. zaupnost celovitost ločevalno jedro verifikacija dokazovalni pomočnik confidentiality integrity separation kernel verification proof assistant true false false Slovenski jezik Angleški jezik Magistrsko delo/naloga 2025-11-11 11:15:08 2025-11-11 11:15:15 2025-12-15 04:08:50 0000-00-00 00:00:00 2025 0 0 0000-00-00 NiDoloceno NiDoloceno NiDoloceno 0000-00-00 0000-00-00 0000-00-00 37810 259367171 Luetic_Ana_-_Formalizacija_locevalnega_jedra_z_uporabo_dokazovalnega_pomocnika.pdf Luetic_Ana_-_Formalizacija_locevalnega_jedra_z_uporabo_dokazovalnega_pomocnika.pdf 1 20B74AC7A4AC25D3CF5A46DAA706A939 b8399e1cf827fb19b89740d887ffdfd25b97bfaca824eabf7502a67640ac7e81 fcd909f7-bee6-11f0-9328-0050569b8976 https://repozitorij.uni-lj.si/Dokument.php?lang=slv&id=221769 Fakulteta za računalništvo in informatiko 0 0 0