Summer Research Fellowship Programme of India's Science Academies

Information-Flow Security Certification of Spark Programs

Ayushi Rastogi

Department of Computer Science and Engineering, National Institute of Technology Uttarakhand, Srinagar Garhwal Uttarakhand 246174

R.K. Shyamasundar

Faculty, Department of Computer Science and Engineering, Indian Institute of Technology, Bombay 400076


Spark Programming Language is a safety strategic language dealing in high security demanding domains particularly in military, medical, bank, space and aviation. Though being a rigorous safety enforcing language, it falls short in leaky termination and progress leak preventions. The existing language is found unguarded and in resistant to explicit and implicit information flow that creeps out a plausible hazard in security systems. This project implements dynamic labelling axioms to present additional syntax and semantics for Ada-Spark Language that would enforce security checking for Ada-Spark language. Syntax and semantics are written using K framework to generate a parser that would check information flow safety for different flow statements. K framework is a formal analysis tool that provides platform to rewrite executable semantics. The aim of this part of project is to associate labels with each identifier and whenever particular construct like assigning statement or iterative statement or sequential statement is encountered, based upon particular semantic action framed in K framework is invoked to ensure flow safety along with maintenance of program counter label that keeps the sensitivity of current context and avoids unnecessary rebuff of declaring executing program as unsafe. Successful execution of correct semantic actions based upon particular construct would prune the non termination and insecure information flow limitations from the existing Spark language making it achieve desired secure proficiency.

Keywords: dynamic labeling implementation, language based security


Statement of the Problems

Desirable and secure Information flow is necessity for preservation of confidentiality and integrity. Providing Information Flow security using programming language, called Language based Security is a proficient methodology to enforce application security using programming language properties that additionally checks the flow sequence along with preservation of program behaviour at the compile time to built a robust and secure system. Information flow describes the path of flow of various inputs and outputs that could be given access to and exposed to various other subects and objects running in environment. Flow security is a state of art to make the exposed subjects' and objects' information secure in lue to provide access of sensitive context to legitimate person having rights to perform permissible operations only. Spark is a critical language that aims to provide inambiguous and secure applications certified by ​Bernard A. Carré, 1985​ and ​J. G. P. Barnes, 2003​ and intends to build up a highly secure, integrated software. Though the language is reliable and insecurity resistant but par beyond it falls in pit of shortcomings in regards to termination insensitivity and leaky information. The following points are pacified to illustrate briefing about the aforementioned anomalies:

  • Termination Insensitivity: Program's pattern of termination that is whether it terminates or not, trades off reliability as it runs on the price of security. It may generate guess as demonstrated in ​​W. Rafnsson, et al, 2016​​ regarding some secure information in the way of program responding to an input. This leaking information permission is imperfect in security notion called as termination insensitive flow is undesirous glitch in present Spark Programs. Divergence of nontermination action based upon sensitive and confidential information fall short and directly irresistant of any cover on its side henceforth is a potential creep that could create an undesirous flow of information to be accessed by unauthorized identity for that particular context ​​A. Askarov, et al, 2008​​. The following code snippets from ​​W. Rafnsson, et al, 2016​​ demonstrate a demand in perfectly written Spark Program to offer some methodology to perge an unhandled glitch that goes undetected in the referred code. For inference to clarify above statement let H referred in Code 1 be a secretive information which can be guessed as an odd or even number based upon either the program prints character "!" on screen or the while loop does not terminate, henceforth exposing the last bit of secretive H information.
  • Progress Insensitivity: Termination insensitivity stated above is a generic guess about a single bit information but an intermediate tracking variable can reveal confidential information progressively to public giving access to impermissible read information. Code 2 from ​W. Rafnsson, et al, 2016​ clearly pacifies progressive revealing of secretive information H via K that prints ASCII value of characters in increasing fashion until H value is achieved.
  1. procedure Leak (H:in out Byte) is
  2. begin
  3. H:=H;
  4. if H mod 2 = 0 then
  5. while True loop
  6. H := H;
  7. end loop;
  8. end if;
  9. Write(Standard Output, Character'Pos('!'));
  10. end Leak;
Information leak via Termination insensitive loop in Spark Program 
  1. procedure Leak (H:in out Byte) is
  2. K: Byte := 0;
  3. begin
  4. H := H;
  5. while True loop
  6. Write(Standard Output, K);
  7. if K >= H then
  8. while True loop
  9. H := H;
  10. end loop;
  11. end if;
  12. K := K + 1;
  13. end loop;
  14. end Leak;
Progressive information leak in Spark Program 


The uses of dimension of additional information flow security serves as a complete safety package of sensitive information in nut shell. Inclusion of additional K semantics helps to prevent intruders man in middle attack attempt as it does not provide read and write facility to illegitimate user.

Major contribution through our presented work can be summarized as follows:

  • Inclusion of flow safety for additional security against undesirous flow.
  • Apprehension and implementation of axiomatic rules to detect and solve glitches of termination insensitivity in Spark Program so as to lay additional provision to deal with aforementioned situation.
  • To propose K Syntactic and semantic actions for each type of statement are designed in concurrent with dynamic labelling axioms for desired information flow that performs halting semantic action on illegitimate flow of information that breaches flow safety.



A Note on confinement problem by ​​Butler W. Lampson, 1973​​ introduces crutiality and seriousness of issue of safety breach along with presentation of few desired characteristic properties of flow within subject to make it reliable. It brings to light various benchmark that must be satisfied inorder to achieve desired information flow but does not present any methodology to address the issue and provide a potential solution over the problem. Denning's A Lattice model of secure information flow ​Dorothy E. Denning, 1976​ actually works to provide an efficient method to address the issue by providing foundation guidelines for secure and safe flow of information to direct research to actual core of the problem that needs to be addressed. His lattice model envisions the schematic and logical flow that an application's subjects are bound to adhere. Though it stands outstanding in presenting novel idea but it does not provide implementation view to carry out the presented approach. Built on same concept ​​Peter J. Denning, 1977​​ presents certification methodology of information flow based upon previously proposed lattice model but fails to track current context sensitivity. ​R.K. Shyamasundar, 2014​ and ​​R.K. Shyamasundar, 2015​​ presents the solid grounds to address the problem but lacks in real implementation of same to systematically enforce the desired theory to practically applied methodology using some tool.

The Dynamic Labelling axioms presents the desired information flow based upon labels to support most sensitive areas that requires high sense of reliability and soundness and must coercively rejects the execution of subjects that tries to breach the security level and attempts to read or write to inaccessible information. ​​N. V. Narendra Kumar, 2018​​ has successfully been able to propose an efficient labelling algorithm to track flow for various type of statements.

DL Algorithm for various statements The following figure is a snapshot from ​​N. V. Narendra Kumar, 2018​​ that has proposed the Dynamic Labelling algorithm

dl algo.png
    DL algorithm from ​N. V. Narendra Kumar, 2018

    Implementation of these axioms in parsing phase at compilation time is still pondering and open challenge to Language based security research community that we attempt to address by designing additional syntax and semantic action for spark program using executable semantics application called K Framework. This sorts and asserts the existing Spark program to perge non termination and insecure information flow limitations to be combined with newer designed axiomatic approach of flow safety via K semantics for prosing and advancing more reliable operations.


    The literature discussed is eye-catching and has tried to scour solutions for addressal of issue but did not provide realistic implementation methodology for achieving the same. Our generous efforts directs to design a practical implementation of presented information to remodel existing Spark Programs with aforementioned glitches of termination insensitivity and progress insensitivity, to provide newer level of information flow security.


    Language Definition and Syntax

    We have put forth our efforts to propose a simple imperative language that along with existing Spark program would enforce flow security. Program insensitivity and termination insensitivity would be pruned that could be verified formally using hoare logic for proposed Spark program with flow security language rules. Language definition for proposed language is given as K syntactic rules in the following snippet.

    1. syntax AExp ::= Id | String
    2. | AExp "+" AExp [left, strict]
    3. | "Loc" "(" Int ")" [strict]
    4. | AExp "#" AExp [left, strict]
    5. syntax Par ::= Par Par | "(" Par ")" [bracket]
    6. | Id "," String ";"
    7. syntax Stmt ::= "procedure" Id | Par
    8. | "Loc" "(" Int ")" ">>>" String ";"
    9. | Id ">>" AExp ";" [strict(2)]
    10. | Id "=" AExp ";" [strict(2)]
    11. >Stmt Stmt
    12. | "Str" Ids ";"
    13. | "print" "("AExps")" ";"
    14. syntax Pgm ::= Stmt
    15. syntax Ids ::= List{Id,","}
    16. syntax AExps ::=List{AExp, ","}
    K-Syntax for Flow Secure Language

    Keyword strict represented in square bracket depicts strictness attribute which is a special K notion to denote reduction of particularly referred operand to a base value, called KResult. Associativity and preference order of evaluation for an operator is mentioned in apprehension of strictness attribute as keyword left. Strictness attribute without argument entails reduction of each operand to base value subsequently followed by operation on resultant values.


    The configuration of proposed language is a set of generally available cells along with special register wrapped in core cell for instance T cell depicted in Code 4. The language proposed consists of special register called nextLoc is annotated to keep track of next available memory. Store cell act as memory representation that utilises map data structure to keep the values of declared objects in program. "." in K-Configuration represents nothing it symbolises to initialise an empty cell. Out cell serves as printing buffer for outstream. K cell and env cell are computational cell and environment cell of K-framework that support computations and static and dynamic bindings respectively.

    1. configuration <T color="yellow">
    2. <k color="green"> $PGM:Pgm ~> execute </k>
    3. <env color="LightSkyBlue"> .Map </env>
    4. <store color="red"> .Map </store>
    5. <out color="Orchid" stream="stdout"> .List </out>
    6. <nextLoc color="gray"> 1 </nextLoc>
    7. </T>
    Configuration for Flow Secure Language


    The proposed language is defined to provide an easy and understandable K semantics depicted in following code snippet are in accordance with Dynamic labelling algorithm to ensure flow security for an assignment and sequence statements keeping in track of current context sensitivity, pc label is assigned memory at the initial growing point of stack. Labels are considered as String types and are used to denote access rights that are used in building Information flow lattice for assurance of safety and security of objects. Look up rules are to find base value from corresponding object bound to some location in environment contained in store. Variable declaration rules and value assignment rules performs required bindings to environment and store the assigned value to place. Macro is declared to provide functionality of multiple declarations as a single statement. Structural rules are enforced aptly to perform sequential execution of statements. Semantics for Execute statement initialises maps of Environment and store cell with defined values.

    1. // AExp
    2. rule <k> Loc(L) => I ...</k>
    3. <store>... L |-> I ...</store> [lookup]
    4. rule <k> Loc(L) >>> I ; =>. ...</k>
    5. <store>... L|->(S => I) ...</store>
    6. rule <k> procedure X => . ...</k>
    7. <env> Env => Env[X <- 0] </env>
    8. <store>... .Map => 0 |-> "P" ...</store>
    9. rule P1:Par P2:Par => P1 ~> P2
    10. syntax KItem ::= "execute"
    11. rule <k> execute =>. </k>
    12. <env> Env </env>
    13. <genv> .Map => Env </genv> [structural]
    14. rule X:Id , E:String ; => Str X; X >> E; [macro]
    15. rule X =I:String;=> X>>I ; ~> Loc(0)>>>I ;
    16. syntax KItem ::= "undefined"
    17. rule <k> Str X:Id; => . ...</k>
    18. <env> Env => Env[X <- L] </env>
    19. <store>... .Map => L |-> undefined ...</store>
    20. <nextLoc> L => L +Int 1 </nextLoc>
    21. rule Str X1:Id, X2:Id, Xs:Id; => Str X1; Str X2, Xs; [macro]
    22. rule <k> X:Id =>I ...</k>
    23. <env>... X |-> N ...</env>
    24. <store>... N |-> I ...</store> [lookup]
    25. rule <k> X>>I:String;=>. ...</k>
    26. <env>... X |-> N ...</env>
    27. <store>... N |-> (_=>I) ...</store> [assignment]
    28. rule S1 + S2 => S1 # S2 # Loc(0) when S1 =/=String S2
    29. rule S1 + S2 => S1 # Loc(0) when S1 ==String S2
    30. rule S1 # S2 => S1 +String S2
    31. // Stmt
    32. rule S1:Stmt S2:Stmt => S1 ~> S2 [structural]
    33. rule Str Ids ;=> . [structural]
    34. syntax Printable ::= String
    35. syntax AExp ::= Printable
    36. context print(HOLE:AExp, _);
    37. rule <k> print(P:Printable,AEs => AEs); ...</k>
    38. <out>... .List => ListItem(P) </out>
    39. rule print(.AExps); => . [structural]
    K Semantics for Flow Secure Language for assignment statement


    K-Syntactic and Semantics actions were tested for assignment statement by passing the following procedure as input program that is designed in accordance with underlying proposed language to inspect the execution of rules and the results obtained marked the concurentness of proposed work with practical applicability as shown in fig. 2. Results obtained are in consonance with expected outcome. Pc variable that keeps the track of current context updates as likely on the execution of statement as required to keep the flow safety assure and does not allow illegitimate information flow. nextLoc Cell updates to next available position for object storage along with desired sequential statement execution rule.

    1. procedure Pc (X,"a"; Y, "b";)
    2. Str Sum;
    3. P , "f";
    4. Q , "m";
    5. Sum =X+Y;
    6. print("Sum value: ",Sum, "\n Pc value: " ,Loc(0));
    7. Str res;
    8. res =P+Q;
    9. print("\n Res value: ", res,"\n Pc value: " ,Loc(0));
    Input Program



      The proposed work lays the basic foundation and novel approach to implement the presented idea to add Spark Program along with Language based security. K Framework serves as a useful tool by providing platform to design effective syntactic and semantic actions that are to appended to existing Spark compiler to provide an additional functionality of flow safety. Executable semantics have marked the authenticity of devised action based upon the type structure of statement that is whether the statement is assignment or sequential, selection or iteration. Iteration statement is still in progress to achieve the final stamp of completion. Proposed implementation has served as wrapping of extra ability to meet safety benchmarks giving a proficient implementation of same for a Spark Program.

      In future, we wish to extend the proposed work to implement RWFM to give the finer and toned configuration of same proposed work that would not only generate labels and keep track of flow but also maintain minute details about owners, readers and writers as well.


      I would like to express my deepest appreciation to all those who provided me the possibility in successful completion of the work. I pay a special gratitude to my guide Prof. R.K Shyamasundar under the Summer Research Fellowship 2019, whose contribution in stimulating suggestions and direction, helped me to coordinate the chosen project.

      I would be indebted to Sandip Ghoshal sir, PhD scholar at IITB for providing his worthy suggestions and valuable encouragement in lue to find better implementation of work directing focus to potential solution that helped me figure out a methodology for feasible implementation.

      K Framework Tool provides technical support and allows various users to connect through mailing list which has helped me a lot to connect with world wide researchers related with this tool to solve unintentional errors and mistakes. I would sincerely thank Rikard Hjort, a K mailing user belonging to same community for sharing his insights in dealing with K Framework along with notion to work on platform with more ease and comfortably.


      • Jean-Francois Bergeretti, Bernard A. Carré, 1985, Information-flow and data-flow analysis of while-programs, ACM Transactions on Programming Languages and Systems, vol. 7, no. 1, pp. 37-61

      • J. G. P. Barnes, High integrity software: the spark approach to safety and security. Pearson Education, 2003.

      • W. Rafnsson, D. Garg, and A. Sabelfeld, \Progress-sensitive security for spark," in International Symposium on Engineering Secure Software and Systems. Springer, 2016, pp. 20{37.

      • A. Askarov, S. Hunt, A. Sabelfeld, and D. Sands. Termination-insensitive noninterference leaks more than just a bit. In ESORICS, pages 333–348, Oct. 2008.

      • Butler W. Lampson, 1973, A note on the confinement problem, Communications of the ACM, vol. 16, no. 10, pp. 613-615

      • Dorothy E. Denning, 1976, A lattice model of secure information flow, Communications of the ACM, vol. 19, no. 5, pp. 236-243

      • Dorothy E. Denning, Peter J. Denning, 1977, Certification of programs for secure information flow, Communications of the ACM, vol. 20, no. 7, pp. 504-513

      • N.V. Narendra Kumar, R.K. Shyamasundar, 2014, Realizing Purpose-Based Privacy Policies Succinctly via Information-Flow Labels, 2014 IEEE Fourth International Conference on Big Data and Cloud Computing

      • N.V. Narendra Kumar, R.K. Shyamasundar, 2015, POSTER, Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security - CCS '15

      • Sandip Ghosal, R. K. Shyamasundar, N. V. Narendra Kumar, 2018, Static Security Certification of Programs via Dynamic Labelling, Proceedings of the 15th International Joint Conference on e-Business and Telecommunications

      Written, reviewed, revised, proofed and published with