Enforcing information flow policies by a three-valued analysis

Abstract

This paper presents an approach to enforce information flow policies using a three-valued type-based analysis on a core imperative language. Our analysis aims first at reducing false positives generated by static analysis, and second at preparing for instrumentation. False positives arise in the analysis of real computing systems when some information is missing at compile time, for example the name of a file, and consequently, its security level. The key idea of our approach is to distinguish between negative and may responses. Instead of rejecting in the latter cases, we type instructions with an additional type, unknown, indicating uncertainty, possibly preparing for a light instrumentation. During the static analysis step, the may responses are identified and annotated with the unknown security type, while the positive and negative responses are treated as is usually done. This work is done in preparation of a hybrid security enforcement mechanismWe prove that our type system is sound by showing that it satisfies non-interference. The novelty is the handling of three security types, but we also treat variables and channels in a special way. Programs interact via communication channels. Secrecy levels are associated to channels rather than to variables whose security levels change according to the information they store. © 2012 Springer-Verlag Berlin Heidelberg.