Jump to Header Jump to Main Content Jump to Footer

NSF CAREER Award seeds development of innovative, highly secure computer language

Home > Blog > NSF CAREER Award seeds development of innovative, highly secure computer language

NSF CAREER Award seeds development of innovative, highly secure computer language

Photo: Bill Harrison and Adam Proctor

Harrison and computer science postdoc Adam Proctor discuss work on the programming language ReWire. Photo by Hannah Sturtecky

“Every electronic gizmo that is mission- or life-critical to the [United States] government must be certified by the National Security Agency,” said MU computer science Professor William Harrison. “What we have developed is a high-level [programming] language that can be used to prove things or verify security of electronic components.”

Harrison said the initial idea for the new language, called ReWire, came out of his 2008 NSF CAREER Award work titled “Automatic synthesis of high assurance security kernels” — research that took aim at language-based security for electronic devices.

Photo: Bill Harrison points at his computer screen

MU computer science Professor William Harrison looks at a circuit diagram in connection with his work developing a new programming language that will prove a system is secure. Photo by Hannah Sturtecky

Harrison’s ReWire collaborators include Gerard Allwein with the Naval Research Lab (NRL), and Adam Procter, now a postdoc in computer science at MU who has worked with Harrison since 2006. Procter’s dissertation is rooted in the development of the unique computer language.

Allwein met Harrison at the NRL when the latter gave a colloquium at the end of a summer appointment at the lab.

“His work interested me, and we got to talking and exchanged emails. There were common themes in our work that would allow us to work together,” said Allwein. “A lot of what we do is multidisciplinary, and we each could expand into different areas.”

Allwein is an algebraic logician; Harrison and Procter are skilled in language semantics and functional programming.

“We can apply what we know about software to hardware with Bill’s language. With mathematical semantics, we can tell what’s being said in hardware design. And on top of that, we can layer mathematical distributed logics on it,” Allwein said. “You must have a mathematical domain to apply semantics.”

This research is especially timely as electronic devices grow increasingly smaller. Instead of discrete components, systems now consist of integrated circuits with all components on a single small chip.

“You have to carry power with you for everything that goes on in an airplane. Discrete components are all weight. But chips are small and low power,” explained Allwein as an example of why systems-on-a-chip are an attractive option.

On the other hand, a “bug” in a discrete component will affect only that component, but with an integrated circuit, that same bug might threaten the entire system. This is where the research group’s programming language comes in.

Graphis: Circuit diagram of a secure processor built with ReWire.

Circuit diagram of a secure processor built with ReWire. Designing circuits in ReWire enables engineers to prove that their systems are secure via rigorous, formal mathematics.

ReWire allows for correctness and security: Does the hardware do what it is supposed to do and are there any security holes in it?

“I developed a compiler, a tool that takes hardware design in mathematical language that links to things that can run on a chip,” said Procter.

“Mistakes are exposed through a regime of testing — trying to break something in one way,” Procter said. “And we’re dealing with the reality that people are hiding bugs in various places. ReWire assists humans in finding them with a framework for expressing mistakes. It’s high assurance deductive verification versus normal, mathematical proof, which can be small. It’s an interactive proof tool. It’s important.”

There are a lot of trends where future architectures will do more complicated things with hardware such as processors and graphics with lots of functionality on specialized hardware. Security becomes embedded in hardware, not software as it is now.

Harrison has made some great connections, and ReWire is being put through its paces at some very high levels.

Australian Chris North has been working with the ReWire team since February. He is group leader for Active Security Technologies in the Cyber & Electronic Warfare Division within Australia’s Department of Defence. One of his group’s primary foci is the development of trustworthy systems — those with high guarantees that they will operate correctly and securely.

Photo: Bill Harrison and his research group

William Harrison poses with members of his research group. From left to right: Adam Proctor, Harrison, Seth Kurtenbach, Tom Reynolds and Chris Hathhorn. Photo by Hannah Sturtecky

Australia is a participant the Cyber Strategic Challenge Group (CSCG), run by The Technical Cooperation Program (TTCP), an international organization of five partner countries — Australia, Canada, New Zealand, the United Kingdom and the United States — that collaborates in defense scientific and technical information exchange.

North’s trustworthy systems group has been collaborating with Harrison’s crew through the TTCP with funding provided by the NSA in 2013 as part of an intergovernmental agreement.

The ReWire developers describe the “five eyes” TTCP group as one that exchanges research and product development to find cross domain solutions to security problems.

“They want to make sure the products are bulletproof,” said Allwein.

North was introduced to Harrison and his work through NRL and the CSCG Trustworthy Systems work. They subsequently invited Harrison to participate in an Australian workshop focusing on the research topic of “mixed levels of trust.”

As part of its TTCP work, Australia is developing design patterns and architectures for trustworthy systems where components of the system may have varying levels of trust.

“Whilst we may not have full trust in some components of the system, for example the processor or the reprogrammable logic chips, we require high assurance that the resulting system will operate correctly,” said North. “The ReWire language is one of the technologies that we are using in developing these systems. It is being used for those portions of the circuit design that are critical to the correct operation of the overall system.”

Harrison is pleased that ReWire is being tested for use at some of the highest assurance levels of security in the world through CSCG. He anticipates that TCCP will fund the research to take the software to the next level.

“There’s nothing like it,” he said. “It’s revolutionary.”

Back to Top

Enter your keyword