Compile-Time Security Certification of Imperative Programming Languages

  • Sandip GhosalEmail author
  • R. K. Shyamasundar
  • N. V. Narendra Kumar
Conference paper
Part of the Communications in Computer and Information Science book series (CCIS, volume 1118)


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.



The authors thank the Ministry of Electronics and Information Technology (MeitY), Govt. of India, for the generous support to the Information Security Research & Development Center (ISRDC) at IIT Bombay.


  1. 1.
    Ghosal, S., Shyamasundar, R.K., Kumar, N.V.N.: Static security certification of programs via dynamic labelling. In: Proceedings of the 15th International Joint Conference on e-Business and Telecommunications, ICETE 2018 - Volume 2: SECRYPT, Porto, Portugal, 26–28 July 2018, pp. 400–411 (2018)Google Scholar
  2. 2.
    Denning, D.E., Denning, P.J.: Certification of programs for secure information flow. CACM 20(7), 504–513 (1977)CrossRefGoogle Scholar
  3. 3.
    Volpano, D.M., Irvine, C.E., Smith, G.: A sound type system for secure flow analysis. J. Comput. Secur. 4(2/3), 167–188 (1996)CrossRefGoogle Scholar
  4. 4.
    Denning, D.E.: A lattice model of secure information flow. CACM 19(5), 236–243 (1976)MathSciNetCrossRefGoogle Scholar
  5. 5.
    Myers, A.C., Liskov, B.: Protecting privacy using the decentralized label model. ACM TOSEM 9(4), 410–442 (2000)CrossRefGoogle Scholar
  6. 6.
    Myers, A.C.: JFlow: practical mostly-static information flow control. In: Proceedings of 26th ACM Symposium on POPL, pp. 228–241 (1999)Google Scholar
  7. 7.
    Myers, A.C., Zheng, L., Zdancewic, S., Chong, S., Nystrom, N.: Jif: Java information flow (2001).
  8. 8.
    Simonet, V., Rocquencourt, I.: Flow Caml in a nutshell. In: Proceedings of 1st APPSEM-II Workshop, pp. 152–165 (2003)Google Scholar
  9. 9.
    Stefan, D., Russo, A., Mitchell, J.C., Mazières, D.: Flexible dynamic information flow control in the presence of exceptions. CoRR abs/1207.1457 (2012)Google Scholar
  10. 10.
    Ryan, P., McLean, J., Millen, J., Gligor, V.: Non-interference, who needs it? In: Proceedings of 14th IEEE CSF Workshop, pp. 237–238 (2001)Google Scholar
  11. 11.
    Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. Sel. Areas Commun. 21(1), 5–19 (2003)CrossRefGoogle Scholar
  12. 12.
    Hicks, B., King, D., McDaniel, P.: Jifclipse: development tools for security-typed languages. In: Proceedings of Workshop on PLAS, pp. 1–10 (2007)Google Scholar
  13. 13.
    Goguen, J.A., Meseguer, J.: Security policies and security models. In: IEEE Symposium on SP, p. 11 (1982)Google Scholar
  14. 14.
    Askarov, A., Sabelfeld, A.: Tight enforcement of information-release policies for dynamic languages. In: Proceedings of 22nd IEEE CSF Symposium, pp. 43–59 (2009)Google Scholar
  15. 15.
    Austin, T.H., Flanagan, C.: Efficient purely-dynamic information flow analysis. In: Proceedings of the ACM SIGPLAN 4th Workshop on PLAS, pp. 113–124 (2009)Google Scholar
  16. 16.
    Zheng, L., Myers, A.C.: Dynamic security labels and static information flow control. Int. J. Inf. Secur. 6(2–3), 67–84 (2007)CrossRefGoogle Scholar
  17. 17.
    Hammer, C., Snelting, G.: Flow-sensitive, context-sensitive, and object-sensitive information flow control based on program dependence graphs. Int. J. Inf. Secur. 8(6), 399–422 (2009)CrossRefGoogle Scholar
  18. 18.
    Stefan, D., Russo, A., Mitchell, J.C., Mazières, D.: Flexible dynamic information flow control in haskell. ACM SIGPLAN Not. 46, 95–106 (2011)CrossRefGoogle Scholar
  19. 19.
    Broberg, N., van Delft, B., Sands, D.: Paragon for practical programming with information-flow control. In: Shan, C. (ed.) APLAS 2013. LNCS, vol. 8301, pp. 217–232. Springer, Cham (2013). Scholar
  20. 20.
    Buiras, P., Vytiniotis, D., Russo, A.: HLIO: mixing static and dynamic typing for information-flow control in Haskell. In: ACM SIGPLAN Notices, vol. 50, pp. 289–301. ACM (2015)MathSciNetCrossRefGoogle Scholar
  21. 21.
    Robling Denning, D.E.: Cryptography and Data Security. Addison-Wesley Longman Publishing Co., Boston (1982)zbMATHGoogle Scholar
  22. 22.
    Le Guernic, G.: Automaton-based confidentiality monitoring of concurrent programs. In: Proceedings of 20th IEEE CSF Symposium, pp. 218–232 (2007)Google Scholar
  23. 23.
    De Groef, W., Devriese, D., Nikiforakis, N., Piessens, F.: FlowFox: a web browser with flexible and precise information flow control. In: Proceedings of ACM CCS, pp. 748–759 (2012)Google Scholar
  24. 24.
    Hedin, D., Birgisson, A., Bello, L., Sabelfeld, A.: JSFlow: tracking information flow in Javascript and its APIs. In: Proceedings of 29th Annual ACM SAC, pp. 1663–1671 (2014)Google Scholar
  25. 25.
    Bichhawat, A., Rajani, V., Garg, D., Hammer, C.: Information flow control in WebKit’s JavaScript bytecode. In: Abadi, M., Kremer, S. (eds.) POST 2014. LNCS, vol. 8414, pp. 159–178. Springer, Heidelberg (2014). Scholar
  26. 26.
    Barnes, J.G.P.: High Integrity Software: The Spark Approach to Safety and Security. Pearson Education, London (2003)Google Scholar
  27. 27.
    Zdancewic, S., Zheng, L., Nystrom, N., Myers, A.C.: Secure program partitioning. ACM Trans. Comput. Syst. (TOCS) 20(3), 283–328 (2002)CrossRefGoogle Scholar
  28. 28.
    Efstathopoulos, P., et al.: Labels and event processes in the asbestos operating system. In: Proceedings of 20th ACM SOSP, vol. 39, pp. 17–30 (2005)Google Scholar
  29. 29.
    Zeldovich, N., Boyd-Wickizer, S., Kohler, E., Mazières, D.: Making information flow explicit in HiStar. In: Proceedings of 7th Symposium on OSDI, pp. 263–278 (2006)Google Scholar
  30. 30.
    Krohn, M.N., et al.: Information flow control for standard OS abstractions. In: Proceedings of 21st ACM SOSP, pp. 321–334 (2007)Google Scholar
  31. 31.
    Cheng, W., et al.: Abstractions for usable information flow control in Aeolus. In: USENIX Annual Technical Conference, pp. 139–151 (2012)Google Scholar
  32. 32.
    Austin, T.H., Flanagan, C.: Permissive dynamic information flow analysis. In: Proceedings of the 5th ACM SIGPLAN Workshop on PLAS, p. 3 (2010)Google Scholar
  33. 33.
    Hritcu, C., Greenberg, M., Karel, B., Pierce, B.C., Morrisett, G.: All your IFCException are belong to us. In: IEEE Symposium on SP, pp. 3–17 (2013)Google Scholar
  34. 34.
    Hunt, S., Sands, D.: On flow-sensitive security types. ACM SIGPLAN Not. 41, 79–90 (2006)CrossRefGoogle Scholar
  35. 35.
    Buiras, P., Stefan, D., Russo, A.: On dynamic flow-sensitive floating-label systems. In: Proceedings of IEEE 27th CSF Symposium, pp. 65–79 (2014)Google Scholar
  36. 36.
    Stefan, D., Russo, A., Buiras, P., Levy, A., Mitchell, J.C., Maziéres, D.: Addressing covert termination and timing channels in concurrent information flow systems. ACM SIGPLAN Not. 47, 201–214 (2012)CrossRefGoogle Scholar
  37. 37.
    Denning, D.E.R.: Secure information flow in computer systems (1975)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • Sandip Ghosal
    • 1
    Email author
  • R. K. Shyamasundar
    • 1
  • N. V. Narendra Kumar
    • 2
  1. 1.Department of Computer Science and EngineeringIndian Institute of Technology BombayMumbaiIndia
  2. 2.Institute for Development and Research in Banking TechnologyHyderabadIndia

Personalised recommendations