Runtime verification of declassification for imperative programs: Formal foundations

Declassification is required for most programs which manipulate protected data to process their results. In highly-secure programs, the declassification decision must be taken explicitly, which means that data or operations which are being declassified are known. This decision is critical and must be supported by automated verifications, which determine the risk of information leakage related to a given declassification. Currently, the available techniques are based on static analysis, which perform an over-approximation of this risk. In this paper, we study how dynamic approaches can perform more precise analysis on what is declassified and where, and finally ensure the security property, which allows declassification, at runtime. The notion of dynamic analysis w.r.t. to non-leakage properties is studied from a theoretical point of view and this proof of concept is illustrated using a ¿While¿ language.