Information flow analysis by abstract interpretation

摘要: Protecting the confidentiality of information stored in a computer system or transmitted over public network is relevant problem security. The goal this thesis to provide both theoretical and experimental results towards design an flow analysis for automatic verification absence sensitive leakage. Our approach based on Abstract Interpretation, theory sound approximation program semantics. We track dependencies among program’s variables using propositional formulae, namely Pos domain. study main ways improve accuracy (by combination abstract domains) efficiency widening narrowing operators) analysis. reduced product logical domain suitable numerical domains yields strictly more accurate with respect ones already literature. modular construction our allows deal trade-off between by tuning granularity abstraction complexity operators. Finally, we introduce Sails, new tool mainstream languages like Java, that does not require any manual annotation. Sails combines leakage different heap abstractions, inferring programs dealing complex data structures too. applied SecuriBench-micro suite preliminary outline effectiveness approach.