  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.
