Secure System (for seL4)

Successful attacks against computer systems worldwide by external hackers and malicious insiders are growing. The secure system prototype in this app demonstrates a trusted computing base (TCB) concept building on the formally-verified seL4 microkernel that will be highly effective against deterring these growing threats.

The system demonstrated in this project will be "unhackable.” An “unhackable” system has the following properties: (1) the risk (and expense) of an external hacker's theft or damage of sensitive data will be far greater than the reward and (2) the probability of theft by a malicious insider will be reduced to very near zero.

The threats posed by external hackers were proved to be preventable in the recently completed DARPA HACMS project, as described in several recent articles. The HACMS project has shown that technology required to prevent data loss and damage by external hackers can be prevented using technology (seL4) that is mostly available today. This app is intended to give a simple demonstration of how to construct a secure system prototype using the seL4 microkernel as a hypervisor for multiple Java Virtual Machines (JVMs).

Read more about the technical details of the system proposed here in the three articles below that were recently published on ACM's Ubiquity website at http://ubiquity.acm.org.

Insider Attacks are a Bigger and Harder Threat?
http://ubiquity.acm.org/blog/insider-attacks-bigger-harder-threat/

Cybersecurity skeptics now embracing formal methods: an interview with Gernot Heiser and Jim Morris
http://ubiquity.acm.org/article.cfm?id=3081880

10 Rules for an Unhackable Data Vault
http://ubiquity.acm.org/article.cfm?id=3081882

The prototype demonstrated here obviously runs on Android, not on seL4. However, as the secure system diagram at the top of the Play Store page clearly shows, the prototype is intended to eventually run ONLY on an underlying seL4 operating system (NOT Windows, NOT Android, and NOT *nix). Once a JVM has been ported to seL4, this prototype will form the initial middleware for a secure system using seL4 as a TCB.

This demonstration hypothesizes four secure clients communicating with a secure server. All communication between client and server is encrypted using Station-to-Station (STS) protocol. A successful STS exchange generates a 256-bit AES encryption key. After the key is used in the next three communication sessions, a new key must be generated using STS. The key expires in the demo if a client is idle for 10 or more seconds. Authentication between client and server is performed using a password stored on all four clients and the server. No systems other than those with the proper stored password can communicate with any node in the proposed system.

After a JVM is successfully ported to seL4, the clients and the server will all be immune to hacking by external hackers and malicious insiders. In such a system it will not be possible for a stored password (or any other data) to be stolen by either insiders or outsiders.

Three simple operations are available to clients in this prototype: (1) encryption loop test, (2) show directory, and (3) retrieve file. The retrieved file is a PDF file of about 1.5 megabytes. After a file is received, the number in parentheses shows the decryption time on your Android device. My smartphone is a Samsung Note 5. The decryption time on my Note 5 is about 80-120 milliseconds, demonstrating that encryption and decryption will be a very small percentage of the overall transmission time.

To run the app in automatic mode (let the system do all the work while you watch the action), type "0.0.0.0" into the field that asks for an IP address, then click "Accept IP Address." This simulates the clicking of buttons in the four clients.

To run the app by clicking the buttons yourself, type "localhost" into the IP address field, then click "Accept IP Address." You can click any enabled button in any of the four clients.