Security and reliability of embedded software have been deeply studied during the last decades: a vulnerability or bug in the software embedded into a safety critical device might have disruptive consequences. Given the limited hardware resources of these devices, embedded software was written in low-level languages (e.g., C and C++). Thus, sound static analysis became a common approach to find issues of this software.
During the last few years, the IoT revolution changed the scenario: IoT devices have usually more resources, and they are connected to the Internet. While there is not yet a de-facto mainstream programming language to develop IoT software, Java is one of the main players. Google recently introduced Android Things, a new Android framework tailored towards IoT devices.
However, although both security and reliability concerns are as relevant for IoT software as for embedded software, there is not yet a sound static analyser targeting IoT Java software.
The goal of this project is to develop a comprehensive support for sound static analyses of Android Things IoT software. In particular, we plan to
develop a specification language, generic w.r.t. a particular IoT support and programming language, to define the IoT architecture, and its privacy and integrity constraints, and
apply this language to the most important components of Android Things support (namely, Google Weave, Google IoT support library, and Google IoT Cloud).
On the one hand, such effort will allow the team led by prof. Merro at University of Verona to apply their theoretical knowledge on semantic foundations and
security issues on IoT systems to a practical and possibly disruptive scenario (Android Things). On the other hand, thanks to this project, Julia will be in position to develop novel static analysis techniques targeting Android Things applications in the short period, and IoT software in the long run. Since Julia is one of the few sound static analysers for generic Java software, its extension to Android Things software could open both scientific and commercial terrific opportunities.
