Tracking Dependent Information Flows

Ensuring the compliance of developed software with security requirements is a challenging task due to imprecision on the security guidelines definition, and to the lack of automatic and formal means to lead this verification. In this paper, we present our approach that aims at integrating the formal specification and verification of security guidelines in early stages of the development life cycle by combining the model checking together with information flow analysis. We formally specify security guidelines that involve dependent information flows as a basis to lead formal verification through model checking, and provide precise feedback to the developer.