Mastering Non-Functional Properties of Software: Energy, Time, Security

In this age of digital mobility, the world increasingly relies on embedded systems run by multicore computing applications. More often than not, this parallel software is requested to maximize energy efficiency while simultaneously coping with severe time constraints and stringent security requirements. And that's where things get a tad tricky. Indeed, although effective analyses exist to predict the energy usage of multicore systems, either alone or in combination with timing information, they are still mostly performed by external tools, after first versions of the code have been written. In fact, while developers write programs to express what they want to do, they do not have the possibility to also express non-functional properties such as energy, timing and security in their source code. Programmers are thus hard-pressed to reason about these in a formal way at source code level, which is precisely the challenge project TeamPlay aims at tackling.
“In any computer program, there is a number of non-functional properties such as time, security or energy. Our goal is to enable programmers of multicore systems to express these properties in a more explicit and easier way than what could be done until now, ” sums up Olivier Zendra, a scientist with Tamis, an Inria research team specializing in cybersecurity . “We want these developers to be able to specify, say, which part of the program must take so much time as a maximum, so much energy as a maximum, or which part of a program will be triggered only if such or such amount of energy is still available, or which part is critical or not, which part must have such level of security vis-à-vis a given threat, so on and so forth. ”
In order to do that, “we must obviously set our eyes on a level of abstraction that the programmer will find pleasant to juggle with. Meanwhile, we will have to go down the whole development stack as well, and make sure that the properties expressed at the higher level can effectively be implemented at lower level to have them executed by the system. The difficulty, obviously, consists in bridging these different levels while having non-functional and functional properties working together. An additional difficulty lies in the fact that security properties are more in their infancy than energy or timing, for example. ”

Six Academic Partners

Started in January 2018, the project will span over a period of three years, gathering eleven partners, six from the academe, five from the industry, each providing a specific focus in the project. On the academic side, it comprises: University of Saint-Andrews (language expressivity), University of Bristol (energy modelling of processors), University of Amsterdam (temporal analysis), Technical University of Hamburg-Harburg (compiling), University of Southern Denmark (unmanned aerial systems) and Inria. “As far as Inria is concerned, we  work on the security aspects. Given my background (A specialist of object-oriented languages, Olivier Zendra co-created SmartEiffel, the GNU Eiffel compiler during his PhD thesis), I  focus on expressiveness at language level. Also involved are my colleagues Axel Legay, head of Tamis, a specialist of program verification, and Annelie Heuser, a specialist of side-channel attacks. We also plan to hire research engineers and/or postdoctoral researchers, with openings for the equivalent of two full-time positions. ”

Five Industrial Stakeholders

The project also gathers five industrial stakeholders. “They  provide us with use cases that will greatly help us disseminate our research findings. AbsInt, for instance, is a German company that supplies compilers and program analysis tools for the verification of safety-critical software. Conversely, Thales Alenia Space Spain is more of an end-user wishing to integrate these new technologies in its workflow. Being in the satellite communication business, they obviously have a keen interest in the time and energy issues. ”
In Danemark, Sky-Watch has none too different preoccupations. “They develop professional drones for mapping and surveillance purposes. One of their goals is to minimize power consumption, not just for the engine but also for other aspects of the system. They are interested in explicitly running their program from the energy point of view so that they can decide to shut a non-critical function in order to extend the mission duration or, conversely, opt for shortening the mission but keeping a function they really need despite it being power-hungry. ”
Energy is also an important parameter for Irida Labs. This Greek company specializes in computer vision for devices ranging from action cameras to industrial robots. “They are interested in decision making with regard to power consumption, which is crucial in the context of embedded systems. For instance, one can choose to change the level of the video quality in order to cope with the amount of energy still available. ”
Located in Rennes, a stone's throw away from Inria center, French company Secure-IC has made a name in protecting embedded devices against cyber-physical attacks. “They will be Tamis' industrial counterpart in the field of security. They plan to integrate into their products these aspects of explicitly-expressed levels of security. They are also interested in energy and time because of side-channels attacks: in certain conditions for instance, energetic or timing behaviors can leak information which a hacker might try to retrieve. ”
The project is expected to result into a number of prototypes that will eventually be interconnected. “Partners work on different aspects but, eventually, each tool must fit into a coherent set echoing a common expression. This is all the more important since our work is meant to spread to the industry and be of practical use. ”