{'fraction_non_alphanumeric': 0.03202452042487978, 'fraction_numerical': 0.008191090207683771, 'mean_word_length': 4.994298384542287, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 1, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 4, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
An Axiomatic Approach to Detect Information Leaks in Concurrent Programs

Realizing flow security in a concurrent environment is extremely challenging, primarily due to non-deterministic nature of execution. The difficulty is further exacerbated from a security angle if sequential threads disclose control locations through publicly observable statements like print, sleep, delay, etc. Such observations lead to internal and external timing attacks. Inspired by previous works that use classical Hoare style proof systems for establishing correctness of distributed (real-time) programs, in this paper, we describe a method for finding information leaks in concurrent programs through the introduction of leaky assertions at observable program points. Specifying leaky assertions akin to classic assertions, we demonstrate how information leaks can be detected in a concurrent context. To our knowledge, this is the first such work that enables integration of different notions of non-interference used in functional and security context. While the approach is sound and relatively complete in the classic sense, it enables the use of algorithmic techniques that enable programmers to come up with leaky assertions that enable checking for information leaks in sensitive applications.


I. INTRODUCTION
Information flow control (IFC) in sequential and concurrent programs has been an active area of research for over two decades. While researchers have developed specification approaches [1], [2], [3], [4] and enforcement mechanisms for sequential programs [5], [6], [7], [8], [9], [10], [11], flow security in concurrent programs remains a challenge primarily due to covert channels that could leak secret information. Timing channels in concurrent programs are the most commonly known covert channels.  For instance, often programs encode secret information in such a way that allow an attacker to learn about confiden-tial data by observing time variations between interleaving execution of assignments to public variables or output statements such as print, or the availability of shared resources in a particular time interval. Recent flow security enforcing mechanisms for sequential programs [12], [6] identify information leaks in individual threads, but the approaches are too restrictive for programs that reveal the control position through the observable output statements. For example, consider the program shown in Figure 1, (Cf. [13]) where h is a secret variable, and await command is a conditional critical region. The await command essentially represents a number of standard synchronization primitives including semaphores. Let us suppose that process T 1 holds the semaphore and executes the critical region as an indivisible operation. Then, output 'acdb' arising due to concurrent executions of T 1 and T 2 reveal the value of h as 0. There have been a few efforts aiming to prevent timing leaks in concurrent or multi-threaded programs [14], [15], [16], [17], [18], [19], [20], [21] but majorly have sidestepped the issue that arise due to output statements.
In this paper, we aim to preserve the confidentiality of programs in a concurrent context preventing an attacker external to the system from gaining knowledge about secret information through observations of program outputs. We describe an axiomatic approach that establishes functional correctness [22] in a parallel context to realize the insecurity at a program point that might leak information due to concurrent executions. In the envisaged work, we introduce auxiliary time variables that capture execution time for each execution step and enables us to derive a notion of leaky assertion for each public program locations, that when satisfied, one can conclude that the program leaks out information. Enforcing functional noninterference in a concurrent setting that uses leaky assertions leads to the identification of plausible information leaks at various program locations. Our proposed approach is primarily motivated by approaches used by Lamport and Schneider [23], [24], [25], [26] on the correctness of real-time distributed programs. Similar to these approaches using time as an ordinary variable for specifying and reasoning about real-time systems, we we arrive at leaky assertions using an external time variable. With such a specification leaky and standard assertions for concurrent programs, we check for non-interference using verification conditions similar to those used in 'Gries-Owicki' [22]. By showing the program is noninterference, we infer information leaks through the leaky assertions embedded in the specification.
Main contributions of the paper are: 1 Introduction of leaky assertions when embedded in concurrent program specifications, enables detection of information leaks once the proof of components of the concurrent programs are shown to be correct when considered in isolation and are further shown to be interference free. 2 Demonstration of the method of embedding leaky assertions in standard concurrent program specification [22], can be used to assert information leaks, from which the information leaks are detected. 3 Checking for information leaks due to public observers like IO and time sensitive operations (those that could disclose program locations through output statements or observable timing channels), in non-interferring flow secure concurrent programs [27]. Rest of the paper is organized as follows. Section II provides an abstract syntax of the concurrent language. Section III briefly describes the necessary background on correctness of concurrent programs and non-interference. Section IV illustrates our solution followed by a formal description of our approach and proof of soundness in Section V. Section VI compares our approach with other related work in the literature, followed by conclusions in Section VII.

II. LANGUAGE SYNTAX
Before proceeding with the solution, we shall briefly describe the syntax of the language we use.
Let s ranging over set S be the set of commands, x be the set of variables ranging over X, and e denote an expression. Language primarily comprises basic actions such as skip, assignment, sequence and control statements such as conditional branch, iteration, await as in [22]. In addition, we consider two statements print(e) and delay(e) that serve as observable points from the perspective of security and hence, these statements are often termed public statements. Statement print(e) writes e , where . denotes the classic evaluation of expressions, into the standard output file that is visible to public. On the other hand, delay(e) postpones the current execution for e time units. The abstract syntax of the language is given below: Operator s 1 s 2 denotes a parallel (or concurrent) composition of sequential programs s 1 and s 2 . The await command is a conditional critical region, that turns a statement s into an indivisible action, is executed in a state that satisfies condition b. The semantics of sequential part of our language essentially follows the classical while-language. Whereas, the semantics for concurrent composition and await statements are in line with the transition rules given in [28].

III. CORRECTNESS OF CONCURRENT PROGRAMS
The seminal work of Hoare [29] provided a basis for establishing axiomatic correctness of imperative programs. Let P and Q be assertions referred to as pre-condition and postcondition for program/statement S. Hoare's triple specification for partial correctness of program S, is denoted {P }S{Q} with the following interpretation: if pre-condition P is true before execution of S, then post-condition Q holds if and when the execution of S terminates.
Owicki and Gries [22] generalized Hoare's axiomatic approach for shared variable concurrency with the introduction of non-interference (functional) of programs. Let S i for i =1,...n, be sequential programs. S 1 S 2 · · · S n denotes concurrent composition. The effect of concurrent execution is the same as executing each S i as an independent program if the programs are disjoint. If the programs are not disjoint, then, it is necessary that programs be interference free. Non-interference requires that assertions used in the proof {P i }S i {Q i } for each process remain validated under concurrent execution of the other processes. Let, T be a statement in program S i . Then, concurrent execution of Formal definition is given below.
Definition 1 (Correctness). Given a proof {P }S{Q} and a statement T with the pre-condition pre(T ), the statement T is said to be non-interfering with {P }S{Q} if the following two conditions hold: where, S ′ is an await or assignment statement within S but not within an await block.

IV. CAPTURING INFORMATION LEAKS THROUGH OUTPUT
The crux of our approach lies in setting observers from which one can draw inference about information leaks. Observation points allow us to deduce how long a process could wait at a control point relative to another process at some other control point wherein the two processes share information via shared variables (could be sensitive) through synchronization. This is realized through auxiliary variables that are used in the specification of concurrent programs. Lamport [25] illustrates an effective use of auxiliary variables for establishing correctness of real-time programs.
Timing constraints for the waiting time that impose upper or lower bound for an action to occur can be expressed using auxiliary (time) variables. Semantic characterization of time constraints required for mutual exclusion and analysis of bounded waiting time is similar to that shown in [25].

A. Illustrative Example
Let us illustrate that the labelled program T 2 showin in Figure 2, where labels denote identifiers for statements as well as locations of program control does indeed leak information via public statements. Labels l 0 and l 8 are the entry and exit labels respectively. Let us mark the execution time of the program at specific program locations using auxiliary variable t. Execution of statements l 3 to l 5 is subject to availability of l0 : t = T print('c'); l1 : if h then l2 : await sem>0 then l3 : sem = sem -1; l4 : v = v+2; l5 : sem = sem + 1 else l6 : skip; l7 : t = t ′ print('d'); l8 :  Figure 1) with auxiliary variable t sem, and hence, involves a delay, say ∆t. Now, an observer can easily measure the intermediate time difference between execution of public statements l 0 and l 7 and just a comparison with ∆t would enable him to deduce that information in h more deterministic (informally, cardinality of the set of possible values gets reduced from the original set of possibilities) than he could infer otherwise.
In short, our approach is based on specifying postulates of leaky assertions at expected control points in the program and establish correctness of the program in a standard manner. Once the proof is established, the leaky assertions locations indicate the points of leakage of information; the actual path can be derived using the semantic rules of the language for the program.
Thus, embedding leaky assertions in the specification of functional correctness (Definition 1) of programs leads to a proof system that enables asserting leaks in the programs . Let S to be an assignment or a non-nested await statement from the thread T 1 . Let P and Q be pre-and post-conditions of S respectively. Then, proof of {P }S{Q} asserts that the leaky assertions hold when T 1 and T 2 execute concurrently.
))} Note that the leaky assertions successfully capture the execution time inconsistencies for both the cases where semaphore sem is locked or released by the process T 1 . Therefore, the assertions remain unaffected by the pre-and post-conditions for any statement S in T 1 . As the assertions always hold good, this invariably proves the program as leaky. Remarks: It is interesting to understand the impact if the program contains a delay statement; suppose the statement skip is replaced by delay(50) -a delay of 50ms (milliseconds for instance). Now, consider the following cases with respect to the leaky assertions: 1 ∆t ≪ 50ms : It would be difficult to postulate leaky assertion as an observer cannot easily determine the execution path for h = 0 or h = 1; hence, the program may be considered secure even though it may not be; note that axiomatic proof is relative to the specifications.

V. FORMALIZATION OF OUR APPROACH
In our two-language approach for establishing leaks, if we can show that assertions at various program points imply information leaks, then we would have established that the program is not-secure; in other words, it is leaky. Thus, if we establish that the program is insecure, we would have established a counter-example; on the other hand, if we establish that the program is secure, it would imply that the program is secure relative to the given specification. Below, we establish the first from which the second follows naturally.
Definition 2 (Leaky Assertion). For a given set of assertions a 0 , . . . , a n at respective control points ℓ 0 , . . . , ℓ n of the given program S, using a nonempty set of sensitive (or high) variables h 1 , . . . , h m of the program, is said to be leaky if a i determinizes the value of at least one of its' sensitive variables, say h j .
As discussed earlier, we say that an execution is leaky if the proof of the program does not invalidate any of the leaky assertions.
Definition 3 (Leaky Execution). Given a proof of {P }S{Q} (we ignore global invariant as given in [22]), where S is an assignment or non-nested await statement, and a program T with at least one output statement with leaky assertion A as it's pre-condition, concurrent execution of S and T is said to be leaky if the following two conditions hold: Issues of completeness also follow on the same lines.
Application to Flow Security: Dynamic labelling (DL) algorithms [30] are in use for compile-time flow security certification. For a program performing IO, however, the DL algorithm could also be effectively used for identifying program points for arriving at leaky assertions at plausible control points. DL algorithm binds subjects and objects of a program with the given static or dynamic labels from a security lattice [31] and evaluates the program as per the flow policy that enforces information flow only in upward direction of the lattice. For standard output, a static label low is assigned denoting least confidential policy. The output statements controlled by sensitive variables that are labelled with higher security labels would cause an information flow from higher label to low, violating flow policy; thus, the algorithm easily highlights public statements with possible sensitivities. Now, one could visualize the interactions of the various concurrent components that could possibly interfere in the functional sense. Using such an intuition, one could come up with different leaky assertions that would detect information leaks. The process of finding information leak in programs that perform IO could be automated through the following steps: (i) first use DL algorithm to identify the public statements that could leak information; (ii) capture time-sensitivity for deriving leaky assertions corresponding to those public statements using various analysis tools or oracles; (iii) arrive at possible interaction of components at these public locations, and (iv) apply model checkers to check for certain properties in components assuming possible assertions in other components. We are working on arriving such algorithmic techniques for detecting information leaks.

VI. RELATED WORK
In this section, we briefly highlight some of the important approaches in the literature to prevent timing leaks in concurrent settings. In particular, we focus on the solution that prevents leaking information through publicly observable control points.
Our idea is primarily motivated by the work shown in [22], [32], [33]. The first one presented flow proof rules that use correctness properties given in [22]. The last two approaches have given a semantic interpretation of non-interference using Hoare-like logic. However, the goal of the above approaches is to establish flow security of programs, whereas we aim to find information leaks due to IO statements and time-sensitive operations using simple inference.
Le Guernic [13] first envisages the potential danger in the use of output statements in concurrent programs, and initial solution that motivated us to provide an alternative approach in the form or security assertions. In this approach, the author develops a run-time monitor that works in tandem with a security automaton to decide whether to allow, deny or modify executions of output statements and synchronization commands, particularly those appear in a branch conditioned on sensitive variables. The automaton forbids executions of output statements in this situation. Further, it acquires locks of synchronization command before evaluating such a conditional. For instance, acquiring semaphore sem in the program shown in Figure 1 would prevent from outputting "acdb". The approach provides a thoughtful solution; nonetheless, it is too restrictive. E.g., in the absence of an output statement, say print('c'), the program is harmless, but as per the above solution executing the program would still be dangerous. The axiomatic approach proposed in this paper removes such restrictions on the program. Our approach enables us to assert flow insecurity in the program methodically through the "Gries-Owicki" conditions for functional correctness, thus overcomes the cases of false alarms.
Other than the above approach, the majority of the mechanisms found in the literature to prevent timing leaks in concurrent programs are based on either (i) developing a sound typing rules to enforce secure-flow properties in concurrent programming languages [19], [21]; (ii) performing source transformation to balance the time variation or eliminate the timing channel [18], [20], [34]; or (iii) developing a run-time monitor to identify potentially dangerous executions that could leak information [14], [35], [36].

VII. CONCLUSIONS AND FUTURE WORK
In this paper, we have proposed an axiomatic proof system using leaky assertions placed at output statement locations. To the best of our knowledge, we are the first to propose an axiomatic approach using approaches for establishing correctness of real-time distributed programs to analyze information leaks in concurrent programs that have observable public locations, leading to the following advantages: (i) it enables to formally prove the presence of information leaks; (ii) aids in integrating the notions of non-interference used in functional and security contexts with respect to complete information flow models like that of Dorothy Denning [31], for shared variable programs.