Projects

Static Security Analysis of IoT Systems

Collaborators: Agostino Cortesi, Fausto Spoto (University of Verona, Italy), Amit Mandal (SRM University, Amaravati, India)

IoT systems usually comprise several software layers: the embedded software running on the physical device (aka thing), some edge application that locally manages a physical system composed by several things and is connected to Internet, some cloud applications providing access to, and storing and visualizing data of the IoT system, and some mobile applications that allows a user to manage the system remotely. Since the overall system interacts with the physical world through sensors and actuators, it is essential to consider the overall system when looking for security vulnerabilities and leakages of sensitive information.

In such context, existing static analysis techniques (and in particular taint analysis) focus on single applications. The goal of this project is to extend such techniques in order to perform inter-program analyses that can detect vulnerabilities due to the interaction between different software layers.

Bibliography

Static Taint Analysis for Privacy

Collaborators: Luca Olivieri, Fausto Spoto

Taint analysis has been successfully applied to detect injection vulnerabilities in Web applications. Such approach consists in tracking if something tainted (e.g., user input) coming from a source reaches a sink (e.g., execution of a SQL query) without being sanitized (e.g., properly escaped). Static taint analysis has been proved to scale up to industrial programs. At the end of the analysis one gets only if the tainted data might reach the sink, but not how (i.e., the flow from the source to the sink).

New privacy regulation (such as the EU GDPR) underlined the relevance of proper treatment of sensitive data. In such scenario, static analysis can be applied in order to track how such sensitive data is accessed, managed and leaked. In particular, we worked on the extension of existing taint analysis techniques to the detection of leakages of sensitive data.

Bibliography

  • Pietro Ferrara, Luca Olivieri, Fausto Spoto: “BackFlow: Backward Context-Sensitive Flow Reconstruction of Taint Analysis Results.”, in Proceedings of VMCAI 2020 [LINK]
  • Pietro Ferrara, Fausto Spoto: “Static Analysis for GDPR Compliance.”, in Proceedings of ITASEC 2018 [LINK]
  • Pietro Ferrara, Luca Olivieri, Fausto Spoto: “Tailoring Taint Analysis to GDPR.”, in Proceedings of APF 2018 [LINK]

Static Analysis of .NET Programs

Collaborators: Fausto Spoto, Agostino Cortesi

During the last decade, several semantic static analyzers have been formalized, designed, implemented and adopted to analyze industrial programs. While many of them targeted Java programs, only very few dealt with .NET programs. Therefore, we formalized a translation of . NET bytecode into Java bytecode for static analysis purposes. This approach has been implemented into the Julia static analyzer (a commercial analyzer for Java programs).

Bibliography

  • Pietro Ferrara, Agostino Cortesi, Fausto Spoto: “From CIL to Java bytecode: Semantics-based translation for static analysis leveraging.”, in Sci. Comput. Program., Vol. 191 [LINK]
  • Pietro Ferrara, Agostino Cortesi, Fausto Spoto: “CIL to Java-bytecode translation for static analysis leveraging.”, in Proceedings of FormaliSE@ICSE 2018 [LINK]

Static Analysis of Android Auto[motive] Applications

Collaborators: Amit Kr Mandal, Federica Panarotto, Agostino Cortesi, Fausto Spoto

Smartphone and automotive technologies are rapidly converging, letting drivers enjoy communication and infotainment facilities and monitor in-vehicle functionalities, via the On Board Diagnostics (OBD) technology. Among the various automotive apps available in playstores, Android Auto infotainment and OBD-II apps are widely used and are the most popular choice for smartphone to car interaction. Automotive apps have the potential of turning cars into smartphones on wheels, but can also be
the gateway of attacks. In this work, we defined a static analysis that identifies potential security risks in Android infotainment and OBD-II apps. It identifies a set of potential security threats and presents an actual static analyzer for such apps. It has been applied to most of the highly rated infotainment apps available in Google Play store, as well as on the available open-source OBD-II apps, against a set of possible exposure scenarios. Results show that almost 60% of such apps are potentially vulnerable
and that 25% pose security threats related to the execution of JavaScript. The analysis of the OBD-II apps shows possibilities of severe Controller Area Network (CAN) injections and privacy violations, because of leaks of sensitive information.

Bibliography