Sandip Ghosal
email: sandipsmit@gmail.com

R K Shyamasundar
email: shyamasundar@gmail.com

Information Flow Security Certification for SPARK Programs

SPARK 2014 (SPARK hereafter) is a programming language designed for building highly-reliable applications where safety and security are key requirements. SPARK platform performs a rigorous data/information flow analysis to ensure the safety and reliability of a program. However, the flow analysis is oriented towards establishing functional correctness and does not analyze for flow security of the program. Thus, there is a need to augment the analysis that would enable us to certify SPARK programs for security. In this paper, we propose an analysis to find information flow leaks in a SPARK program using a Dynamic Labelling (DL) approach for multi-level security (MLS) programs and describe an effective algorithm for detecting information leaks in SPARK programs, including classes of termination/progress-sensitive computations. Further, we illustrate the application of our approach for overcoming information leaks through unsanitized sensitive data. We also show how SPARK can be extended for realizing MLS systems that invariably need declassification through the illustration of an application of the method for security analysis of Needham-Schroeder public-key protocol.

Introduction

SPARK [1] is a programming language built on Ada 2012. While the SPARK data flow analysis [START_REF] Barnes | High integrity software: the spark approach to safety and security[END_REF][START_REF] Bergeretti | Information-flow and data-flow analysis of whileprograms[END_REF] primarily emphasizes on establishing functional correctness, the flow security aspect remains neglected. Thus, certifying a program for flow security [START_REF] Denning | Certification of programs for secure information flow[END_REF] is crucial for building reliable and secure applications.

A security property, often referred to as information-flow policy (IFP), governs the flow security certification mechanisms. One of the widely used policies for security certification first advocated in [START_REF] Denning | Certification of programs for secure information flow[END_REF] says: if there is information flow from object x to y, denoted by x → y, then the flow is secure if λ(x) can-flow-to λ(y), where λ is a labelling function that maps subjects (stakeholders of a program in execution) and objects (variables, files) of a program to the respective security label or class which describe the confidentiality and integrity of program values. The security labels together form a security lattice. In this paper, we are concerned with algorithmic techniques for security certifications of SPARK programs that comply with the IFP over a security lattice.

First, we highlight the security aspects of information flow and sanitization of sensitive data in SPARK programs following an assessment of proposed solutions in the literature.

1. Role of Implicit Flows: Two principle flows of information in a program are direct and indirect or implicit flows. A typical example of direct information flow is an explicit assignment of a secret value. Implicit flows arise when the control flow of a program is affected by secret values. Note that often secret information could be encoded in terms of differences in side effects of control flow. Such a property leads to various further classifications, such as terminationsensitive/insensitive or progress-sensitive/insensitive. The work by Rafnsson et al. [START_REF] Rafnsson | Progress-sensitive security for spark[END_REF] was the first exploration towards the flow security in SPARK programs with the focus on termination-and progress-sensitive information leaks. We shall briefly describe the evidence of information leaks as shown in [START_REF] Rafnsson | Progress-sensitive security for spark[END_REF]. a. Termination-insensitive flow analysis in SPARK [START_REF] Rafnsson | Progress-sensitive security for spark[END_REF]: A termination-sensitive flow analysis can track an instance that depends on the program termination. However, it is evident from the example shown in Table 1 that SPARK follows a termination-insensitive flow analysis. Note that the program outputs a character '!' depending on the termination of if block, which eventually terminates if the variable H is an odd number. If H is secret, then the program leaks one bit of sensitive information. The solution proposed in [START_REF] Rafnsson | Progress-sensitive security for spark[END_REF] identifies the terminating loops using termination oracles [START_REF] Moore | Precise enforcement of progress-sensitive security[END_REF] and performs a graph transformation by introducing additional edges going out from potentially infinite loops to the end of the program. Therefore, it extends the dependency in the program and lets SPARK to perform dependency analysis on control flow graphs. While the approach avoids explicit exceptions, it needs to instrument the code from a global understanding, and further, there is no concrete feedback on the reasons for insecurity to the programmer. The main shortcomings of the above solutions are: (i) the transformations are not algorithmic (automatic), (ii) difficult to detect the issues of information leak. Nonetheless, the source-to-source transformation approach of [START_REF] Rafnsson | Progress-sensitive security for spark[END_REF] connects the theory of progress-sensitive non-interference with the practice, the SPARK data flow analysis together with the above approach is insufficient to enforce the classic notion of non-interference [START_REF] Boudol | On typing information flow[END_REF][START_REF] Goguen | Security policies and security models[END_REF][START_REF] Volpano | A sound type system for secure flow analysis[END_REF] while building MLS systems. Thus, it would be nice if an algorithmic strategy could be established that would enable us to overcome the above problems. 2. Sanitizing Data: Another aspect of security in SPARK, as highlighted by Chapman [START_REF] Chapman | Sanitizing sensitive data: How to get it right (or at least less wrong[END_REF], concerns sanitizing sensitive local data in Ada-SPARK programs for building secure applications. The author elaborates potential leaks due to access to "unsanitized" sensitive temporary data, e.g., OS page files or core dump of a running process. For instance, in the simple decryption program shown in Table 3, the local variables N and D become sensitive and, if not sanitized, could leak secret information in S. Chapman demonstrates the issue of Ada language, where an attempt to sanitize sensitive data is suppressed by the compiler while performing optimization. In SPARK, the sanitization step is ineffective as it does not influence the final exported value. The discussion arises questions like: How do we define 'sensitive' ? What objects in the program are 'sensitive' ? How are they identified? The author prescribes one possible solution, i.e., adopting coding policies to sanitize sensitive local data in the Ada-SPARK project, e.g., use of pragma Inspection Point. Further, following the naming convention for the sensitive data, e.g., adding prefixes "Sensitive ", " SAN" to the names of types, variables, would aid the programmer to handle it appropriately. Thus, it must be evident that there is a need to build a succinct definition of "sensitive" data and provide an algorithmic analysis for the compiler/runtime monitor for appropriate treatment.

In this paper, we propose a single alternative solution to the above problems using a dynamic labelling algorithm [START_REF] Ghosal | Static security certification of programs via dynamic labelling[END_REF][START_REF] Ghosal | Compile-time security certification of imperative programming languages[END_REF] that not only helps to identify the sensitive local objects but also detects potential information leaks in SPARK programs, thus alleviate the burden of manual intervention in the source program. The automation receives a list of immutable security labels of global variables as input and generates mutable labels for the local variables while following the IFP throughout the computation. Primarily, objects sensitive to the outside world are considered as global, but the programmer may use her discretion to choose any variable as a global object.

Further, developing a secure application that involves objects with security labels from a multi-point general lattice often demands the need for declassification. We introduce the construct Declassify borrowing the notion of declassification from the security model RWFM [START_REF] Kumar | Realizing purpose-based privacy policies succinctly via information-flow labels[END_REF][START_REF] Kumar | A complete generative label model for latticebased access control models[END_REF] as briefed in the later section.

The main contributions of our work are summarized below: 1. Propose an algorithmic solution for SPARK statements using information flow policies and establish its capability to detect program points that could plausibly leak information. 2. Illustrate the efficacy of our approach in detecting information leaks primarily through termination channels [START_REF] Volpano | Eliminating covert flows with minimum typings[END_REF] or progress channels [START_REF] Askarov | Termination-insensitive noninterference leaks more than just a bit[END_REF] and discuss the advantages, such as localizing possible leaking points, identifying sensitive objects automatically. 3. Introduce "Declassify" construct for SPARK programming language based on the model proposed in [START_REF] Kumar | Realizing purpose-based privacy policies succinctly via information-flow labels[END_REF] and illustrated its usage through an application on a cryptographic protocol.

The rest of the paper is organized as follows. Section 2 provides the necessary background for dynamic labelling algorithm and RWFM flow security model. Section 3 presents a single alternative solution to overcome the shortcoming of SPARK flow analysis using security labels and dynamic labelling algorithm. Section 4 discusses the necessity of declassification as an extension in the SPARK language and illustrate the Declassify construct with an application of Needham-Schroeder (NS) public key protocol. Finally, implementation highlights are given in Section 5 followed by conclusions in Section 6.

Background

In this section, we briefly discuss the dynamic labelling algorithm and provide an overview of a recently proposed flow security model RWFM that is used for labelling subjects and objects and governing information flow transitions while developing an MLS system in SPARK.

Dynamic Labelling Algorithm (DL)[9,10]

Let G and L be the sets of global and local variables of a program, and λ is a projection from subjects, objects, and program counter pc to its' respective security label from the lattice. Function var returns the set of variables appearing in expression e and SV , T V provide the set of source and target variables respectively for a given statement S. The algorithm DL takes three parameters as inputs: basic SPARK statements such as assignment, selection, iteration, or sequence denoted by S; the highest security label cl of the executing subject referred to as clearance; and a labelling function λ where the global variables are mapped to their given immutable labels. If all the local variables are successfully labelled, the algorithm returns a new map λ otherwise flags a message "UN-ABLE TO LABEL" on detecting a possible flow leak. Note that, initially, the mutable labels of all the local variables, including pc are labelled as public (⊥). The algorithm DL for basic control statements of SPARK language is described in Table 4. Here, problem of "insecurity" will be λ1(pc) = λ(pc) ⊕ tmp indicated by one of the recursive calls. λ2 = DL(S1, cl, λ1) if (λ2 = λ1) λ1 = λ2 λ2 = DL(while e then S1 end loop, cl, λ1) return λ2 Note that "UNABLE TO LABEL" yields the control point where a certain object fails to satisfy the information flow policy. [START_REF] Kumar | Realizing purpose-based privacy policies succinctly via information-flow labels[END_REF][START_REF] Kumar | A complete generative label model for latticebased access control models[END_REF][START_REF] Kumar | Poster: dynamic labelling for analyzing security protocols[END_REF]: An overview We provide a brief overview of the Readers-Writers Flow Model (RWFM) for information flow control.

v) λ1 = λ if (tmp cl) then λ1(pc) = λ(pc) ⊕ tmp exit 'UNABLE TO LABEL' if x ∈ L : λ = λ λ1(x) = λ(x) ⊕ λ(pc) ⊕ tmp λ (pc) = λ(pc) ⊕ tmp return λ1 λ1 = DL(S1, cl, λ ) if x ∈ G : λ2 = DL(S2, cl, λ ) if λ(pc) ⊕ tmp ⊕ cl λ(x)

Readers-Writers Flow Model (RWFM)

Definition 1 (RWFM Label) A RWFM label is a three-tuple (s, R, W ) (s, R, W ∈ set of principals/subjects P ), where s represents the owner of the information and policy, R denotes the set of readers allowed to read the information, and W identifies the set of writers who have influenced the information so far.

Definition 2 (can-flow-to relation ( )) Given any two RWFM labels L 1 = (s 1 , R 1 , W 1 ) and L 2 = (s 2 , R 2 , W 2 ), the can-flow-to relation is defined as:

R 1 ⊇ R 2 W 1 ⊆ W 2 L 1 L 2
Definition 3 (Join and meet for RWFM Labels) The join (⊕) and meet (⊗) of any two RWFM labels L 1 = (s 1 , R 1 , W 1 ) and L 2 = (s 2 , R 2 , W 2 ) are respectively defined as

L 1 ⊕ L 2 = (-, R 1 ∩ R 2 , W 1 ∪ W 2 ) L 1 ⊗ L 2 = (-, R 1 ∪ R 2 , W 1 ∩ W 2 )
The set of RWFM labels SC = P × 2 P × 2 P forms a bounded lattice (SC, , ⊕, ⊗, , ⊥), where (SC, ) is a partially ordered set and = (-, ∅, P ), and ⊥ = (-, P, ∅) are respectively the maximum and minimum elements.

Definition 4 (Declassification in RWFM)

The declassification of an object o from its current label (s 2 , R 2 , W 2 ) to (s 3 , R 3 , W 3 ) as performed by the subject s with label (s 1 , R 1 , W 1 ) is defined as

s ∈ R 2 s 1 = s 2 = s 3 R 1 = R 2 W 1 = W 2 = W 3 R 2 ⊆ R 3 (W 1 = {s 1 } ∨ (R 3 -R 2 ⊆ W 2 )) (s 2 , R 2 , W 2 ) may be declassified to (s 3 , R 3 , W 3 )
This says, the owner of an object can declassify the content to a subject(s) only if the owner is the sole writer of the information or that subject(s) had influenced the information earlier.

Our Approach Using Dynamic Labelling Algorithm

Our approach relies on the application of dynamic labelling for the SPARK program. We first extend the set of rules given earlier with the labelling rules for the SPARK procedures as described below. Extended Labelling Algorithm (DL + ) for SPARK Procedure: Consider a procedure call, say p(a 1 , . . . , a m ; b 1 , . . . , b n ) where, a 1 , . . . , a m are the actual input arguments and b 1 , . . . , b n are the actual input/output arguments corresponding to the formal input parameters (mode IN) x 1 , . . . , x m and formal input/output parameters (mode OUT or IN OUT) y 1 , . . . , y n . The dynamic labelling algorithm for SPARK procedure call is shown in Table 5. Once given a procedure call, the DL algorithm first computes the procedure body before returning the control to the caller. The algorithm adheres to the parameters passing mechanisms while transferring the control. Following are the operations the algorithm performs at entry & exit points of the procedure: (i) at the entry point it initializes the labels of formal input parameters with the corresponding labels of the actual input arguments; (ii) creates an instance pc local to the procedure; (iii) initializes the pc and local variables with the mutable label ⊥; (iv) evaluates the procedure body; and (v) finally resets the pc label on exiting from the procedure and returns the final labels to the caller. Note that, the intrinsic property of the labelling algorithm automatically enforces the required security constraints for a procedure call given in [START_REF] Denning | Cryptography and data security[END_REF].

With the extended dynamic labelling algorithm for SPARK statements are in place (Tables 4,5), certifying information flow security for a given SPARK program consists of the following steps: 1. Initialize the labels of global variables for the given SPARK program. 2. Apply the labelling algorithm DL + , for the SPARK program. 3. If the labelling succeeds, then the program has no information leak; if the labelling algorithm outputs the message "UNABLE TO LABEL" it implies there is a possibility of information leak.

Illustration:

First, we apply the algorithm to the programs shown in Table 1, 2, and demonstrate solutions to issues 1(a)-(b) of Section 1. Consider H and Standard Output are the global objects initialized with the immutable labels H and ⊥ (i.e., public) respectively, such that information cannot flow from H to Standard Output, i.e., λ(H) = H λ(Standard Output) = ⊥. Also, we assume that the executing subject has the clearance label H. Then the derived labels of local variables as well as program counter (pc) are shown in the Tables 6,7.

(i) Detecting termination-sensitive information leaks:

In Table 6, it can be observed that since pc reads the variable H its label is raised to H. Now execution of the procedure call Write(Standard Output, Character'Pos('!')) causes a flow from pc to Standard Output, therefore, the label of Standard Output must be at least equal to the label of pc. Since the label of Standard Output is immutable, the algorithm fails to update the label, hence exits by throwing the message "UNABLE TO LABEL". The point of failure detects the location and objects responsible for flow policy violation.

(ii) Detecting progress-sensitive information leaks: Similarly, since the procedure Write(Standard Output, K) causes information flow from both K and pc to Standard Output it needs to satisfy the constraint

  begin N := Get N (S); D := Get D(S); M := (C * * D) mod N ; --Sanitize N and D N := 0; D := 0; end Decrypt;

Table 4 .

 4 Description of Algorithm DL for basic SPARK statements such as assignment, selection, iteration and sequence 1. S : null:: SV(S)={∅}; TV(S)={∅}; DL(S, cl, λ) : return λ 2. S : x := e:: SV(S)=var(e); TV(S)={x}; 3. S : if e then S1[ else S2] end if:: DL(S, cl, λ): SV(S)=SV(S1) ∪ SV(S2) ∪ var(e); tmp = v∈var(e)∩G λ(v) TV(S)=TV(S1) ∪ TV(S2) if (tmp cl) then DL(S, cl, λ): exit 'UNABLE TO LABEL' tmp = v∈var(e)∩G λ(

  then λ3(pc) = λ1(pc) ⊕ λ2(pc) return λ1 ∀x ∈ L : λ3(x) = λ1(x) ⊕ λ2(x) else exit 'UNABLE TO LABEL' return λ3 4. S : while e then S1 end loop:: 5. S : S1; S2;:: SV(S)=SV(S1) ∪ var(e); SV(S)=SV(S1) ∪ SV(S2); TV(S)=TV(S1); TV(S)=TV(S1) ∪ TV(S2); DL(S, cl, λ): DL(S, cl, λ): tmp = v∈var(e)∩G λ(v) return DL(S2, cl, DL(S1, cl, λ)); if (tmp cl) then exit 'UNABLE TO LABEL' λ1 = λ

Table 1 .

 1 SPARK

	program leaking in-
	formation through a non-terminating
	loop.
	procedure Leak (H:in out Byte) is
	begin
	H:=H;
	if H mod 2 = 0 then
	while True loop
	H := H;
	end loop;
	end if;
	Write(Standard Output,
	Character'Pos('!'));
	end Leak;

Table 2 .

 2 SPARK program leaking information progressively.

	procedure Leak (H:in out Byte) is
	K: Byte := 0;
	begin
	H:=H;
	while True loop
	Write(Standard Output, K);
	if K >= H then
	while True loop
	H:=H;
	end loop;
	end if;
	K := K + 1;
	end loop;
	end Leak;

Table 3 .

 3 A simple decryption program written in SPARK.

procedure Decrypt(C: in Integer; S: in Private Key; M : out Integer) is N ,D:Integer;

Table 5 .

 5 DL Algorithm for a Procedure Call 6. S : p(a 1 , . . . , a m ; b 1 , . . . , b n :: DL(S, cl, λ)://Initialize the label of the parametersλ = λ init forall i ∈ 1 . . . m, λ (x i ) = λ(a i ) //Evaluate the body of the procedure λ 1 =DL(p -body, cl, λ ) return λ 1

λ(K) ⊕ λ(P C) λ(Standard Output). But, the algorithm fails to continue as λ(pc) ⊥.

(iii) Identifying sensitive data for sanitization: Here, we shall address the questions and solution related to handling "sensitive" data discussed in Section 1. Note that the labelling algorithm takes the initial classification of sensitive/non-sensitive data and transfer the sensitivity to local variables automatically during computation. Since the algorithm generates the labels of local variables from the given set of sensitive global variables, any attempt to access unsanitized sensitive local objects must satisfy the IFP, thus restrict access as required. Consider the program shown in Table 3 where global objects C, S and M are sensitive data with the label given H. Then applying the dynamic labelling algorithm would compute the labels of local variables N and D as H transferring the sensitivity label of global variables. Thus any attempt to read the sensitive data by a less-sensitive user (or process) would indicate misuse of information flow. Remarks: One can write statements like H = H followed by L = L (H and L are global and denote a high and low variables respectively) somewhere in the program. In such cases, the platform would indicate "UNABLE TO LABEL" as it fails to satisfy the constraint H ⊕ pc L. We ignore such corner cases and leave the onus of correcting the code on the programmer.

3.1 Comparison with Rafnsson et al. [START_REF] Rafnsson | Progress-sensitive security for spark[END_REF] and SPARK Analysis Table 8 provides a comparison of DL + with the SPARK analysis and approach proposed in [START_REF] Rafnsson | Progress-sensitive security for spark[END_REF] in terms of common objectives that are generally sought in the information flow analysis tools. From the comparison it is evident that our approach subsumes the advantages of other two approaches.

Need of Declassification in MLS Systems

Quite often, in a decentralized labelling environment, it is required to relax the confidentiality level and reveal some level of information to specific stakeholders for the successful completion of the transaction. For this purpose, the notion of Declassification or Downgrading needs to be captured either implicitly or explicitly. We shall understand the context from the classic password update problem shown in Table 9.

Consider a function Password Update that updates password database by a new password (new pwd) only if the guess password (guess pwd) provided by the user matches with the old password and updates the result accordingly. Note that there is a need to convey the result as an acceptance of the new password so that the user can use it further. Table 9 shows that the result becomes sensitive data by the time the function returns its value. In the context of the MLS system, passing this sensitive data (i.e., result) to a less-sensitive entity (i.e., user) may violate the information flow policy. Therefore, it demands controlled declassification. There are two possibilities for introducing declassification at the point of returning the value: (i) Have an assertion that ensures declassification explicitly, or (ii) Perform declassification implicitly at the function return.

Declassification in SPARK:

We adopt an explicit declassification mechanism for SPARK. The programmer may localize the program point that needs a declassification and place the construct Declassify to add specific readers. However, the addition needs to be robust as otherwise, the declassification may appear to be a mere discretionary that would have serious consequences in a decentralized model. For this reason, we shall borrow the "Declassification" rule from the RWFM model [START_REF] Kumar | Realizing purpose-based privacy policies succinctly via information-flow labels[END_REF] as briefed in the Section 2.2. Consider p, p 1 , . . . range over the set of principals P , and x ranges over the set of objects/variables. Functions A, R and W have the form f : L → P which map to owner, readers and writers fields respectively for a given security label in the lattice L. Now let us assume principal p executes the statement Declassify(x,{p 1 , . . . , p n }) to add p 1 , . . . , p n into the readers set of a variable x. Then we define the algorithm DL + for the Declassify statement as below: Note that the encrypted message, at step 2.2 obtains a label inaccessible to A, therefore, explicitly declassified by B so that A can decrypt the message for further use. Similarly, A also performs a declassification at step 3.3 so that B can access the data. It follows from the above illustrations that declassification for MLS is essential, and the DL algorithm, along with the RWFM model, ensures appropriate automatic labelling to ensure security properties.

Implementation of DL + for SPARK

The implementation of our approach first generates RWFM labels for the global variables of a SPARK program from the given readers and writers set of respective variables. Once the labels are generated, the set of global variables annotated with the corresponding RWFM labels and the SPARK program are given as input to the dynamic labelling algorithm. The algorithm either outputs the labels of all the intermediate variables or throws the message "UNABLE TO LABEL" in the presence of possible flow leaks. Figure 1 presents a schematic diagram of the implementation. We have analyzed the programs discussed in this paper and tested in a security workbench for Python language under development using the dynamic labelling approach. Table 10. A prototype of a program for N-S public-key protocol [START_REF] Needham | Using encryption for authentication in large networks of computers[END_REF] Program Derived Labels procedure NS Protocol A(--list of parameters) is --Declarations of local objects M a M a (A,{ * },{}) begin pc (S,{ * },{S}) --1) A encrypts N a, Aid using B's key P ub b pc (S,{A,B},{A,B,S}) M a:=Encrypt(Aid,N a,P ub b); M a (A,{A,B},{A,B,S}) --3.1) A decrypts M b using A's key P ri a pc (S,{A},{A,B,S}) M a:=Decrypt(M b,P ri a); M a (A,{A},{A,B,S}) --3.2) A encrypts N a, N b using B's key P ub b pc (S,{A},{A,B,S}) M a:=Encrypt(N a,N b,P ub b); M a (A,{A},{A,B,S}) --3.3) A declassifies M a pc (S,{A},{A,B,S}) Declassify(M a,{B}) M a (A,{A,B},{A,B,S}) end NS Protocol A;

Conclusions

In this paper, we have illustrated how an extended form of dynamic labelling algorithm integrated with RWFM provides an effective platform for flow security certification of SPARK programs, including termination-and progress-sensitive flows. The approach enables us to use an automatic compile-time labelling algorithm for data that aids in detecting information leaks due to termination and progress sensitivity, and unsanitized data. Also, the programmer gets feedback on the reasons for the misuse of information at the specific program point, enables him to refine the program only to realize flow security. These features add to the usability of the program. The approach provides a natural stepping stone for direct/implicit introduction of declassification for programming MLS systems in SPARK, thus preserve end-to-end confidentiality properties. So far, we have experimented on these aspects on our security workbench developed for Python programs. One can further develop an axiomatic proof system that follows naturally on similar lines as proposed in [START_REF] Andrews | An axiomatic approach to information flow in programs[END_REF][START_REF] Denning | Cryptography and data security[END_REF]. One of the distinct advantages of our approach is keeping the SPARK analysis and security analysis orthogonalthus, enabling technology adaptation easily to the SPARK platform.