История изменений
Исправление hateyoufeel, (текущая версия) :
что именно там доказали
Процитирую их сайт для Ъ:
Functional correctness: the C code of all verified configurations of seL4 behaves precisely as specified in the seL4 specification and nothing more. This is the strongest assurance that the code will not have any unspecified behaviour.
Binary correctness: in the configurations that support this property, the binary machine code running on the processor correctly implements the behaviour of the C code assumed in the functional correctness proof. By extension, this means the binary code implements precisely the behaviour of the specification, and nothing more.
Security: in the configurations that support this property, the specification, and by extension the kernel code, prevents an application running on top of seL4 from modifying data without authorisation (integrity), from interfering with resource access of other applications (availability), and from learning information from other applications without explicit authorisation (confidentiality). Together these security properties enforce the isolation of components running on top of the kernel, allowing critical components to securely run alongside untrusted software.
зачем
Зачем нужно ядро, которое 100% гарантированно не вылетит с паникой? Чувак, я даже не знаю.
Кстати, они ещё и компилятор Си породили, который гарантированно выдаёт бинарник с поведением, описанным в исходном коде.
Исходная версия hateyoufeel, :
что именно там доказали
Процитирую их сайт для Ъ:
Functional correctness: the C code of all verified configurations of seL4 behaves precisely as specified in the seL4 specification and nothing more. This is the strongest assurance that the code will not have any unspecified behaviour.
Binary correctness: in the configurations that support this property, the binary machine code running on the processor correctly implements the behaviour of the C code assumed in the functional correctness proof. By extension, this means the binary code implements precisely the behaviour of the specification, and nothing more.
Security: in the configurations that support this property, the specification, and by extension the kernel code, prevents an application running on top of seL4 from modifying data without authorisation (integrity), from interfering with resource access of other applications (availability), and from learning information from other applications without explicit authorisation (confidentiality). Together these security properties enforce the isolation of components running on top of the kernel, allowing critical components to securely run alongside untrusted software.