The more you open your system up to communicate with other devices, the more you make it vulnerable to attack. Simple web pages are no different, and building a secure and stable interface is all it takes to shield your data from malicious activity.
The Internet has transformed the way human beings view and connect with the world. Sharing thoughts, feelings, and views has become as simple typing out 140 characters and hitting send. The classic argument between friends is now ended by a standard Google search instead of hours of lively debate. The Internet is now so embedded in modern day society that not many people understand the “magic” that goes into viewing a simple web page.
Webpages provide some of the simplest ways to arrange information as a visible document. A server at a remote location hosts the data, which it sends through the Internet to the device that requested the information. Because of the massive scale of the internet, the average user never considers how these systems interact. However, large websites are not the only applications that use these protocols. With the speed improvement of embedded devices, smaller systems can now access the Internet, creating the Internet of Things (IoT).
By connecting embedded devices to the Internet, the vastness of the World Wide Web is now available on Smoker Grills and Coffee Roasters. While the positive features of this system are numerous, the negatives are equally widespread and can be devastating. For example, the recent Mirai Botnet was used to continually scan the Internet of Things and infect devices with Malware that can be used for widespread Denial of Service attacks. Developers need to address security when designing Internet connected devices.
DornerWorks developed a sample application for an embedded device that hosts a webpage, allowing anyone on the same local network to access it. This webpage displays the amount of time the server has been active and allows the user to click a button to execute a function on the device.
Compared to massive websites like Amazon, Google, or even smaller websites like this one, this is not impressive. However, this application was built using the CAmkES Architecture on top of seL4, a formally verified microkernel developed by Data61. DornerWorks was able to use seL4 to componentize and isolate each portion of the Web-Server, providing increased security to the device.
lwIP was kind enough to provide an example application that hosts a Web-Server, which DornerWorks ported for seL4 functionality. The lwIP application had two distinct portions:
These portions were split into separate CAmkES components with an interface between them for necessary inter process communication.
The following diagram outlines how the system was constructed. The Ethdriver, HTTPServer, and FileSystem all work together to host the Web Server. The triangle connections represent hardware interrupts; the rectangle connections represent shared dataports; the circle connections represent interfaces.
One of the obvious Web-Server requirements is that the embedded device must have pages to host. Since these smaller embedded systems do not have a dedicated file system, one cannot add or remove files at will. The FileSystem is a custom RAM based component that manages all necessary files. To convert webpages into a format suitable for this system, a python script transforms web pages into the appropriate format. The FileSystem component then links all the files together in a list, which it can search through, read from, and update whenever necessary.
To connect to the internet the Ethdriver component interfaces directly with the hardware to transmit and receive packets regardless of transmission style. The Ethdriver is a reactive component that only processes packets destined for one of its clients. As seen in the diagram above, the HTTPServer is the Ethdriver’s only client.
http:// The HTTPServer component is where the magic happens. The server sets up lwIP to interface with the Ethdriver in order to send and receive the requested data. When a connection is established, lwIP sets up callbacks for Send and Receive events. These events handle sending the requested information to the remote client. Hardware timers are used to update the TCP interval timers and update the information that the webpage is designed to request. The HTTPServer also generates faux-hardware interface, allowing the Web-Server to be automatically attached or removed based on the project’s needs.
The Router sets up a TCP connection on Port 80, which is the default HTTP port. This connection is set to listen for incoming connections from any IP Address, so any device on the same network can connect.
When the web page requests a file, the custom interface between the Router invokes the custom interface between the FileSystem. The Router submits an “open” request, and the FileSystem searches every file for a match. If a match is found, the file information is copied into a shared buffer. The Router uses the actual data and appends the necessary HTTP information before using lwIP and the Ethernet drivers to send the webpage information to the client.
DornerWorks’ Web Server application contains two files that the webpage can request: Time and Print. The web page can make an HTTP GET request for either file. The web server reacts very differently dependent on the file being requested. For every GET request, the web server checks whether the requested file has an associated callback function. This allows the webpage to perform pre-defined commands on the web server!
Physical switches are often used to change the state of a device. For example, smartphones use buttons to take a picture, adjust the volume, or change the lock status. Many manufacturers package embedded devices to prevent physical access to the hardware, which means user input can be challenging without a display. These callbacks allow for web-based user input of embedded devices. In DornerWorks’ example, the Print file contains a callback that prints a message on the serial port. This functionality could be expanded based entirely on the requirements of the project.
Security is a very large factor in designing Internet connected devices. By componentizing the Web-Server using CAmkES, DornerWorks can leverage the formal verification provided by Data61 and be assured that one faulty component cannot access secure data or bring down the entire system.
Do you want your product to interface with the Internet of Things, but are concerned about the security risks? Are you interested in seL4, but it is difficult to work with? DornerWorks designed this example to be easy to adapt to any solution and can provide guidance through the seL4 learning curve.
Even if seL4 isn’t right for you, we would love to assist you in enhancing the security of your product.
This code functions with seL4 7.0 and CAmkES 3.1. DornerWorks has open-sourced this code for the further development of the seL4 Ecosystem.
All of the necessary pieces are hosted on DornerWorks’ github page. The application code can be found here. Instructions for getting and compiling the source code can be found here.
Good Luck and happy coding!
