Type systems equivalent to data-flow analyses for imperative languages |
| |
Authors: | Peeter Laud Tarmo Uustalu Varmo Vene |
| |
Affiliation: | 1. Department of Computer Science, University of Tartu, J. Liivi 2, EE-50409 Tartu, Estonia;2. Institute of Cybernetics at Tallinn University of Technology, Akadeemia tee 21, EE-12618 Tallinn, Estonia |
| |
Abstract: | We show that a large class of data-flow analyses for imperative languages are describable as type systems in the following technical sense: possible results of an analysis can be described in a language of types so that a program checks with a type if and only if this type is a supertype of the result of applying the analysis. Type-checking is easy with the help of a certificate that records the “eureka”-bits of a typing derivation. Certificate-assisted type-checking amounts to a form of lightweight analysis à la Rose. For secure information flow, we obtain a type system that is considerably more precise than that of Volpano et al., but not more sophisticated. Importantly, our type systems are compositional. |
| |
Keywords: | Data-flow analyses Secure information flow Type systems |
本文献已被 ScienceDirect 等数据库收录! |
|