World's first hack-free software
In future applications, seL4 could ensure that trusted financial transaction software from secure sources like banks or stock exchanges can operate securely on a customer's mobile phone alongside "untrusted" software, such as games downloaded from the Internet, according to its developers.
Lead scientist Gerwin Klein said, "Our seL4 microkernel is the only operating system kernel in existence whose source code has been mathematically proven to implement its specification correctly. Under the assumptions of the proof, the seL4 kernel for ARM11 will always do precisely what its specification says it will do."
No comments:
Post a Comment