My research interests are focused on the application of rigorous mathematical theories to enhance the reliability, security, and performances of software by means of static analysis. Abstract interpretation is a framework applied to develop sound static analyses proving properties on all possible executions of a program. However, approximation is necessary to achieve computability, and the analysis might produce false alarms. Finding a good balance between precision, efficiency, and soundness depends on specific applications, and it usually requires deep research investigation. I am particularly interested in new scenarios where static analysis might have a relevant impact, and I have focused my recent research activity on mobile and .NET software.
In this page you can find an almost exhaustive list of projects I am currently involved in:
- LiSA: Library for Static Analysis
- Security and reliability analysis of smart contracts
- Static analysis of machine learning algorithms
- Static security analysis of IoT systems
- Static taint analysis for privacy (completed)
- Static analysis of .NET programs (completed)
- Static Analysis of Android Auto[motive] Applications (completed)
For a comprehensive view of the projects of the Software and System Verification group, please give a look to this webpage.
Keywords: abstract interpretation, static analysis, mobile programs, software engineering, program verification, multithreading, security.
LiSA
Collaborators: Luca Negrini, Vincenzo Arceri, Agostino Cortesi
LiSA (Library for Static Analysis) aims to ease the creation and implementation of static analyzers based on the Abstract Interpretation theory. LiSA provides an analysis engine that works on a generic and extensible control flow graph representation of the program to analyze. The development of LiSA started in Fall 2020 and we are expecting to release the first stable version by Summer 2021. You can find more information about LiSA in our GitHub repository and the corresponding project website.
Security and reliability analysis of Smart Contracts
Collaborators: Vincenzo Arceri, Fabio Tagliaferro, Imran Alam, Agostino Cortesi
Blockchain and Smart Contracts are growing more and more in popularity thanks to the hype built around these technologies and the wide range of their applications, such as cryptocurrencies, digital securities and identity management.
The possibility of implementing Smart Contract infrastructures using general-purpose programming languages has become widespread, such as in Cosmos or Hyperledger, where, for example, Go language can be involved to build blockchain applications within these frameworks.
Nevertheless, the design of such languages did not have blockchain development as a goal: their use in such context intrinsically inherits the well known general-purpose programming languages problems. Besides, new blockchain-related vulnerabilities arise in such a context: representatives are transaction ordering and timestamp manipulation.
The objective of this project is to identify and implement advanced and sophisticated program analysis approaches to enhance the quality of applications, remaining in the context of general-purpose programming languages.
Static Analysis of Machine Learning Algorithms
Collaborators: Stefano Calzavara, Claudio Lucchese
Machine learning has proved invaluable for a range of different tasks, yet it also proved vulnerable to evasion attacks, i.e., maliciously crafted perturbations of input data designed to force mispredictions. In this project we apply static analysis to verify the security of decision tree models against evasion attacks with respect to an expressive threat model, where the attacker can be represented by an arbitrary imperative program.
Bibliography
- Stefano Calzavara, Pietro Ferrara, Claudio Lucchese: “Certifying Decision Trees Against Evasion Attacks by Program Analysis”, in Proceedings of ESORICS 2020 [LINK]
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
- Amit Kr Mandal, Pietro Ferrara, Yuliy Khlyebnikov, Agostino Cortesi, Fausto Spoto: “Cross-program taint analysis for IoT systems.”, in Proceedings of SAC 2020 [LINK]
- Pietro Ferrara, Amit Kr Mandal, Agostino Cortesi, Fausto Spoto: “Cross-Programming Language Taint Analysis for the IoT Ecosystem.”, in ECEASST, Vol. 77 [LINK]
- Amit Kr Mandal, Federica Panarotto, Agostino Cortesi, Pietro Ferrara, Fausto Spoto: “Static analysis of Android Auto infotainment and on-board diagnostics II apps.”, in Softw. Pract. Exp., Vol. 49 [LINK]
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
- Amit Kr Mandal, Federica Panarotto, Agostino Cortesi, Pietro Ferrara, Fausto Spoto: “Static analysis of Android Auto infotainment and on-board diagnostics II apps.”, in Softw. Pract. Exp., Vol. 49 [LINK]
- Federica Panarotto, Agostino Cortesi, Pietro Ferrara, Amit Kr Mandal, Fausto Spoto: “Static Analysis of Android Apps Interaction with Automotive CAN.”, in Proceedings of SmartCom 2018 [LINK]
- Amit Kr Mandal, Agostino Cortesi, Pietro Ferrara, Federica Panarotto, Fausto Spoto: “Vulnerability analysis of Android auto infotainment apps.”, in Proceedings of CF 2018 [LINK]