act interpretation. R. Barbuti, C. Bernardeschi and N. De Francesco With mobile technology more and more prominent, the problem of security leakages becomes more and more important. Due to this importance, the problem of security leakages is extensively studied in the literature. However, since the downloaded code may be an assembly code, this paper studies the problem of secure information flow in stackbased assembly languages. The method used in the paper stract interpretation of the operational semantics, where programs are analysed in order to collect approximate information about their run-time behaviour. The authors define a notion of security, the so-called sigma security, and ficient conditions that the abstract transition system needs to satisfy in order to ensure sigma-security. Since the approach of this paper is semantical, there is a good potential for its automation. The authors exploit this potential and outline the approach of using model checking for checking sigma-sec...
George F. Georgakopoulos, David J. McClurkin