Australiërs komen met 'waterdichte' kernel
Nicta heeft ongeveer vijf jaar gewerkt aan de kernel met een team wiskundigen en een open source verificatietool Isabelle, die aan de Technische Universiteit van München is ontwikkeld.
Shutterstock
Shutterstock
De 7500 regels C-code, waaruit de kernel bestaat, zijn op een groot aantal fouten getest aan de hand van formele wiskundige methoden. De regels zijn daardoor formeel gespecificeerd en formeel geverifieerd. Dat betekent dat elke regel consistent is met de specificaties. Een en ander resulteert in een kernel die onder meer niet bevattelijk is voor buffer overflow-aanvallen.
De kernel is geschikt als basis voor allerhande applicaties, maar Nicta mikt er vooral mee op kritische toepassingen voor de luchtvaartindustrie en defensie.
Volgens de onderzoekers is L4 ook zeer geschikt voor gevirtualiseerde omgevingen. Data kunnen veilig apart opgeslagen worden op dezelfde fysieke server maar logisch en veiligheidstechnisch op gescheiden virtuele servers.
Gerelateerde artikelen
Gerelateerde artikelen
Reacties
Om een reactie achter te laten is een account vereist.
Inloggen Word abonnee