Compile-time security certification of imperative programming languages

With the ever increase in the demand of building secure systems, recent years are witnessing a plethora of research on information flow control (IFC) techniques in programming languages to enforce a finer-grained restriction on the propagation of information among untrusted objects. In this paper, we introduce a dynamic labelling (DL) algorithm (This paper is an extended version of the article [1] presented in SECRYPT’18.) for security certification of imperative programming languages that follows a combination of mutable and immutable labelling referred to as hybrid labelling approach. First, we study the possible methods of binding security labels with the subjects and objects of the program which include program counter that represent implicit flow within a program and compare the precision achieved by the applications of methods on benchmark programs. Next, we describe our labelling algorithm that generates labels for intermediate subjects/objects of a program from the given set of initial labels (some of which could be immutable throughout the computation) adhering to the constraints defined in [2] for a program to be information-flow secure. Apart from the usual control statements found in the imperative languages, we also present the labelling approach for a procedure call highlighting subtleties of different parameter passing mechanisms adopted in modern languages. Further, we discuss a variant of the algorithm for concurrent programs. It is shown that our algorithm always terminates after a finite number of iterations, also establish the soundness concerning non-interference as given by [3]. We compare the labelling precision realizable by our approach with the existing approaches in the literature. © Springer Nature Switzerland AG 2019