Reasoning about inter-procedural security requirements in IoT applications

TL;DR

This paper presents a novel static analysis technique for assessing security properties of IoT applications directly from LLVM bitcode, bridging the gap between formal models and actual implementation behavior.

Contribution

It introduces a workflow combining static analyses and rule-based matching to evaluate security properties from LLVM bitcode, addressing model-implementation discrepancies.

Findings

Effective derivation of formal models from LLVM bitcode

Identification of security property violations in IoT software

Enhanced accuracy in security assessment through combined analysis methods

Abstract

The importance of information security dramatically increased and will further grow due to the shape and nature of the modern computing industry. Software is published at a continuously increasing pace. The Internet of Things and security protocols are two examples of domains that pose a great security challenge, due to how diverse the needs for those software may be, and a generalisation of the capabilities regarding the toolchain necessary for testing is becoming a necessity. Oftentimes, these software are designed starting from a formal model, which can be verified with appropriate model checkers. These models, though, do not represent the actual implementation, which can deviate from the model and hence certain security properties might not be inherited from the model, or additional issues could be introduced in the implementation. In this paper we describe a proposal for a novel technique to assess software security properties from LLVM bitcode. We perform various static analyses, such as points-to analysis, call graph and control-flow graph, with the aim of deriving from them an 'accurate enough' formal model of the paths taken by the program, which are then going to be examined via consolidated techniques by matching them against a set of defined rules. The proposed workflow then requires further analysis with more precise methods if a rule is violated, in order to assess the actual feasibility of such path(s). This step is required as the analyses performed to derive the model to analyse are over-approximating the behaviour of the software.