
'Last Friday, Google announced the release of KataOS, a security-minded operating system focused on embedded devices running ambient machine learning workloads. As Phoronix notes, it uses the Rust programming language and is "built atop the seL4 microkernel as its foundatin." From Google's Open-Source Blog: As the foundation for this new operating system, we chose seL4 as the microkernel because it puts security front and center; it is mathematically proven secure, with guaranteed confidentiality, integrity, and availability. Through the seL4 CAmkES framework, we're also able to provide statically-defined and analyzable system components. KataOS provides a verifiably-secure platform that protects the user's privacy because it is logically impossible for applications to breach the kernel's hardware security protections and the system components are verifiably secure. KataOS is also implemented almost entirely in Rust, which provides a strong starting point for software security, since it eliminates entire classes of bugs, such as off-by-one errors and buffer overflows. The current GitHub release includes most of the KataOS core pieces, including the frameworks we use for Rust (such as the sel4-sys crate, which provides seL4 syscall APIs), an alternate rootserver written in Rust (needed for dynamic system-wide memory management), and the kernel modifications to seL4 that can reclaim the memory used by the rootserver. KataOS code is being worked on via GitHub under the AmbiML umbrella.' -- source: https://tech.slashdot.org/story/22/10/17/2256206 Someone keen to demo this at one of our next meetings? Cheers, Peter -- Peter Reutemann Dept. of Computer Science University of Waikato, NZ https://www.cs.waikato.ac.nz/~fracpete/ http://www.data-mining.co.nz/

On Wed, 19 Oct 2022 10:18:04 +1300, Peter Reutemann quoted:
'KataOS provides a verifiably-secure platform that protects the user's privacy because it is logically impossible for applications to breach the kernel's hardware security protections and the system components are verifiably secure.'
1) Security does not compose. A combination of any number of components that have been proven “secure” and one which has not been proven “secure” is one which has not been proven “secure”. 2) Any system is only as “secure” as its weakest part.
participants (2)
-
Lawrence D'Oliveiro
-
Peter Reutemann