Resource Analysis and Verification for Dependable Embedded Software

EPSRC Funded Project EP/E021948/1

Principal Investigator: Dr. Shengchao Qin

in collaboration with Prof. Wei-Ngan Chin (NUS, Singapore)

Summary:

Embedded software widely exists in home electrical appliances like washing machines, microwave ovens, dryers and dishwashers, in mobile devices like PDAs, navigators, mobile phones and smart cards, as well as in safety critical systems such as military units, medical devices and motor cars. Such systems are often equipped with limited memory footprints due to various constraints on e.g. product size, power consumption and manufacture cost. Paying insufficient attention to resource issues when developing software for such systems may result in a corresponding software failure after deployment. A real example is the anomaly problem of the Mars Rover Spirit which was due to a memory leakage problem ignored in the software development process. In some cases, such software failure may put human lives at risk. It is thus very important to ensure memory safety and guarantee memory adequacy for software running on these systems.

In this project, we study memory safety and memory usage for programs running on embedded devices, where dynamically allocated objects may be present. Our aims are to verify memory safety for such software, to predict statically (i.e. before a program starts to run) and precisely the memory usage bounds and to ensure that such software will never require more memory than the device can provide.

Memory in software systems are typically organised into two main components: stack and heap. Stack is an efficient way for using and recovering memory spaces, and is important for method invocations and transient objects. Heap is used for more complex data structures that may live beyond the method calls where they are created. Our first objective was accomplished by a multiple-pass analysis which infers automatically memory upper bounds on stack and heap usage for assembly-level programs. The focus on low-level programs was mainly because optimising compilers may render memory analyses done at the source level possibly unsafe to use. The initial experimental results have confirmed the viability of the approach ([ISMM08],[TASE10]).

While the stack bound analysis is generally applicable, the heap bound analysis applies only to programs where mutable objects are not shared. Programs with shared and mutable objects were left into the second objective, for which, we decided to follow a logic-based approach as the originally proposed type-based one ([SAS05],[ICSE05]) is lack of a precise and concise way to specify deep heap properties with must-aliasing and size information. This has proven to be a right move as our new specification language (based on separation logic) allows us to capture precise must-aliasing information for shared mutable objects. It also allows us to capture numerical information (size, memory usage, contents) together with shape information via recursively defined predicates. Our verification system based on this expressive specification mechanism can then automatically verify memory safety (e.g. no dereference to null or dangling pointers), as well as memory usage (i.e. to verify that a program would not require more memory than the device can provide), as shown in our implemented system ([ATVA09],[SCP10]). By conducting automated verification on memory safety and memory usage for programs with shared and mutable objects, we have accomplished the second objective.

Our investigation on the second objective also opened up another challenging research problem: can we automatically compute user-annotations on the shape (incl. aliasing) and size (incl. memory usage) information for programs with shared and mutable objects? This problem is undecidable in general, therefore appropriate abstraction mechanisms would be required. This becomes the main focus of another EPSRC-funded project ( EP-G042322).

System:

MemHIP - The memory safety and memory usage verifcation tool.

References: