Tech Xplore: Researchers reveal a new computing platform that is provably secure even alongside software compromised I/O devices
Tech Xplore: Researchers reveal a new computing platform that is provably secure even alongside software compromised I/O devices. https://techxplore.com/news/2021-06-reveal-platform-provably-software-compro...
The reporter makes grandiose claims, but says they are reporting on a hardware platform that sounds like it ensure all bus traffic is e2e encrypted internally, so software and hardware compromises can't easily access it unless they are in the peripheral that produced it. Where's the original paper or lecture?
https://www.cylab.cmu.edu/news/2021/06/15-ioseparation.html Skip to Content <https://www.cylab.cmu.edu/news/2021/06/15-ioseparation.html#maincontent> [image: CyLab] <https://www.cylab.cmu.edu/index.html> Menu A big step towards cybersecurity’s holy grail CyLab researchers reveal a new computing platform that is provably secure even alongside software compromised I/O devices Daniel Tkacik JUN 15, 2021 - - - - - - - <?su=Interesting%20article%20from%20CMU%E2%80%99s%20CyLab%3A%20A%20big%20step%20towards%20cybersecurity%E2%80%99s%20holy%20grail&subject=Interesting%20article%20from%20CMU%E2%80%99s%20CyLab%3A%20A%20big%20step%20towards%20cybersecurity%E2%80%99s%20holy%20grail&body=The%20trek%20towards%20the%20holy%20grail%20of%20cybersecurity%E2%80%94a%20user-friendly%20computing%20environment%20where%20the%20guarantee%20of%20security%20is%20as%20strong%20as%20a%20mathematical%20proof%E2%80%94is%20making%20big%20strides.%0A%0Ahttps%3A%2F%2Fwww.cylab.cmu.edu%2Fnews%2F2021%2F06%2F15-ioseparation.html> The trek towards the holy grail of cybersecurity—a user-friendly computing environment where the guarantee of security is as strong as a mathematical proof—is making big strides. A team of Carnegie Mellon University CyLab researchers just revealed a new provably secure computing environment that protects users’ communication with their devices, such as keyboard, mouse, or display, from all other compromised operating system and application software and other devices. That means that even if malicious hackers compromise operating systems and other applications, this secure environment is protected; “sniffing” users’ keystrokes, capturing confidential screen output, stealing or modifying data stored on user-pluggable devices for example, is impossible. Protection like this has not been possible to date. Virgil Gligor, *Professor*, Electrical and Computer Engineering “In contrast to our platform, most existing endpoint-security tools such as antivirus or firewalls offer only limited protection against powerful cyberattacks,” says CyLab’s Virgil Gligor <https://www.cylab.cmu.edu/directory/bios/gligor-virgil.html>, a professor of electrical and computer engineering (ECE) and a co-author of the work. “None of them achieve the high assurance of our platform. Protection like this has not been possible to date.” The groundbreaking workOpens in new window <https://www.computer.org/csdl/proceedings-article/sp/2021/893400b746/1t0x9DPKE36> was presented by Miao Yu, a postdoctoral researcher in ECE and the team’s lead implementor, at last month’s IEEE Symposium on Security and Privacy, the world’s oldest and most prestigious security and privacy symposium. Specifically, the researchers presented an I/O separation model, which defines precisely what it means to protect the communications of isolated applications running on frequently compromised operating systems such as Windows, Linux, or MacOS. According to the researchers, the I/O model is the first mathematically-proven model that achieves communication separation for *all* types of I/O hardware and I/O kernels, the programs that facilitate interactions between software and hardware components. Imagine that you need to transfer some money online, and the transactions you are about to execute are so sensitive that you’d like a guarantee they will remain private *even if* your computer has unknowingly been compromised with malware. Performing those transactions in this environment would be provably secure; even your completely compromised operating system would be unable to steal or modify the private data you input using your keyboard or mouse and display on your screen. This type of secure environment is even more important with the rise of remote work, as more and more workers are utilizing Virtual Desktop Infrastructures (VDIs) which allows them to operate remote desktops. “Business, government, and industry can benefit from using this platform and its VDI application because of the steady and permanent shift to remote work and the need to protect sensitive applications from future attacks,” says Gligor. “Consumers can also benefit from adopting this platform and its VDI clients to secure access banking and investment accounts, perform provably secure e-commerce transactions, and protect digital currency.” This platform is still in the development phase, but Gligor and his team aims to commercialize it in the coming years. Paper reference An I/O Separation Model for Formal Verification of Kernel ImplementationsOpens in new window <https://www.computer.org/csdl/proceedings-article/sp/2021/893400b746/1t0x9DPKE36> - Miao Yu, Carnegie Mellon University - Virgil Gligor <https://www.cylab.cmu.edu/directory/bios/gligor-virgil.html>, Carnegie Mellon University - Limin Jia <https://www.cylab.cmu.edu/directory/bios/jia-limin.html>, Carnegie Mellon University [image: Carnegie Mellon] <http://www.cmu.edu/> CyLab Security and Privacy Institute Robert Mehrabian Collaborative Innovation Center (CIC) 4720 Forbes Avenue Pittsburgh, PA 15213 +1 412 268 5715 - CyLab TwitterOpens in new window <https://twitter.com/cylab> - CyLab FacebookOpens in new window <https://www.facebook.com/carnegiemelloncylab/> - CyLab YouTubeOpens in new window <https://www.youtube.com/user/cmuCyLab> - CyLab LinkedInOpens in new window <https://www.linkedin.com/showcase/carnegie-mellon-university-cylab> 2020 Carnegie Mellon University /Legal <http://www.cmu.edu/legal/> “We hack because we care about security, and we want to protect people from potential threats by identifying problems systematically.” Yuan Tian, software security researcher in CyLab
https://doi.ieeecomputersociety.org/10.1109/SP40001.2021.00101 Abstract Commodity I/O hardware often fails to separate I/O transfers of isolated OS and applications code. Even when using the best I/O hardware, commodity systems sometimes trade off separation assurance for increased performance. Remarkably, device firmware need not be malicious. Instead, any malicious driver, even if isolated in its own execution domain, can manipulate its device to breach I/O separation. To prevent such vulnerabilities with high assurance, a formal I/O separation model and its use in automatic generation of secure I/O kernel code is necessary. This paper presents a formal I/O separation model, which defines a separation policy based on authorization of I/O transfers and is hardware agnostic. The model, its refinement, and instantiation in the Wimpy kernel design, are formally specified and verified in Dafny. We then specify the kernel implementation and automatically generate verified-correct assembly code that enforces the I/O separation policies. Our formal modeling enables the discovery of heretofore unknown design and implementation vulnerabilities of the original Wimpy kernel. Finally, we outline how the model can be applied to other I/O kernels and conclude with the key lessons learned.
participants (2)
-
jim bell
-
Karl