Formalizacija ločevalnega jedra z uporabo dokazovalnega pomočnikaLuetić, Ana (Avtor) Mihelič, Jurij (Mentor) zaupnostcelovitostločevalno jedroverifikacijadokazovalni pomočnikMed 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 jedra20252025-11-11 11:15:08Magistrsko delo/naloga175859VisID: 37810COBISS_ID: 259367171sl