promotor: prof.dr. M.C.J.D. van Eekelen (RU and OU)
co-promotor: dr. S. Smetsers (RU)
Radboud Universiteit Nijmegen
Date: 1 September, 2015, 14:30
Practically every modern electronic device is controlled by software. It is important to establish properties of this software, such as functional correctness, security or the ability to function with limited resources. Failure of critical systems can be financially costly or even lethal. Functional correctness and security are crucial for safe operation. In a world that is quickly depleted of its resources, energy-efficiency is vital.
This thesis presents a series of software analysis methods, each of which aids the verification or inference of such properties. It focuses on semantic analysis at compile-time and builds upon existing techniques where possible.
Most of this research was done in the context of the GoGreen project, which aims to build a self-learning, secure and energy-efficient smart-home system. Such a system combines wireless sensor nodes to observe a house and the people within its walls with an intelligent algorithm that controls heating, ventilation, lighting and appliances. We focus on properties that are crucial for such a system: functional correctness, security and efficient use of resources.
To protect the system and the privacy of its users, communication between devices in the GoGreen system must be secured by encrypting the stream of information. To enable this, the communicating parties must agree on a (pair of) key(s). Entering a secret key on a wireless sensor node is impossible, due to its limited interface. A solution is to use the Tamper-Evident Pairing protocol, which enables pairing of two devices by pressing a (virtual) button on both devices within a certain time-frame. However, some of the parameters needed to implement Tamper-Evident Pairing are under-specified. In Chapter 2, model-checking is used to analyse Tamper-Evident Pairing and it is discovered that the protocol is vulnerable to attacks if these parameters are not chosen wisely. Model-checking is applied in an iterative fashion to discover what values of the parameters result in a tamper-evident set-up and formulate a constaint ensuring security of the protocol from the results.
For embedded software this is extra important that it behaves according to specification, because it can be very hard to update the software in case errors are detected after release. It must therefore be thoroughly tested. Chapter 3 presents a method to improve coverage of test cases generated by symbolic execution for programs with loops. It works by symbolically executing the loop body out-of-context, i.e. by disregarding constraints over symbolic variables. This can produce models for symbolic variables that execute all branches within the loop body. The symbolic variables can then be concretized to these values.
Wireless sensor nodes are typically battery-powered. The GoGreen system must at least be energy-neutral as a whole, but preferably save energy. It is thus crucial that wireless sensor nodes are energy-efficient. The hardware of the wireless sensor nodes is controlled by embedded software. It is therefore preferable to use energy-efficient implementations. Chapter 4 presents a Hoare logic for energy-consumption analysis. Given a model of the energy-related behaviors of the hardware components, this analysis can statically bound the energy consumption of software running on said hardware. The method is sound and implemented in the tool ECAlogic.
Wireless sensor nodes typically wake up for a short time to do their work, then go back into an energy-saving mode. Their program must be able to execute within this time-frame. It is therefore important to bound execution time. As most of the execution time of typical embedded programs is spent in loops, it is an important step to bound loop iterations. Furthermore, loop bounds are a prerequisite for analysing consumption of any resource, as a certain amount of resources (possibly bounded) can be consumed on every iteration. Chapter 5 presents a novel method to infer polynomial ranking functions for loops. It instruments the loop with a counter, then runs it for a set of test inputs and interpolates a polynomial over the resulting iteration counts. The set of test inputs is chosen such that it satisfies a condition that guarantees the existence of a unique interpolating polynomial.
To be able to cost-effectively produce wireless sensor nodes, they need to be equipped with just as much memory as they need, not more. It is therefore important to be able to bound memory consumption of their embedded software. Chapter 6 presents the tool ResAna and the underlying resource analysis methods. The loop bound analysis method is further extended with a way to deal with so-called condition jumping. A heap-space analysis is developed, using extensions of the resource analysis tool Costa, which is based on recurrence relation solving. Costa is extended by applying the polynomial interpolation based ranking function inference method to recurrence relation solving, correcting its results for arrays, simplifying its results and adding a Virtual Machine specialisation step. Furthermore, a stack-space analysis is presented. This analysis uses Costa to obtain a measure for recursive functions (analogous to a ranking function for loops), then combines this with data-flow analysis and measured stack frame sizes to obtain a concrete upper bound on the consumed stack space.
This thesis contributes a series of software analysis methods. The methods aid in the establishment of program properties that are of particular interest for resource-sensitive systems, such as security, functional correctness and efficient use of resources.