Options
Using dynamic pushdown networks to automate a modular information-flow analysis
Publikationstyp
Conference Paper
Date Issued
2015-07
Sprache
English
Author(s)
First published in
Number in series
9527 LNTCS
Start Page
201
End Page
217
Citation
Lecture Notes in Computer Science 9527 LNTCS: 201-217 (2015)
Contribution to Conference
Publisher DOI
Scopus ID
Publisher
Springer
In this article, we propose a static information-flow analysis for multi-threaded programs with shared memory communication and synchronization via locks. In contrast to many prior analyses, our analysis does not only prevent information leaks due to synchronization, but can also benefit from synchronization for its precision. Our analysis is a novel combination of type systems and a reachability analysis based on dynamic pushdown networks. The security type system supports flow-sensitive tracking of security levels for shared variables in the analysis of one thread by exploiting assumptions about variable accesses by other threads. The reachability analysis based on dynamic pushdown networks verifies that these assumptions are sound using the result of an automatic guarantee inference. The combined analysis is the first automatic static analysis that supports flow-sensitive tracking of security levels while being sound with respect to termination-sensitive noninterference.
Subjects
Concurrency
Information-flow security
Static analysis
DDC Class
004: Informatik