Skip to main content
SpringerLink
Log in
Book cover

International Conference on E-Business and Telecommunications

ICETE 2018: E-Business and Telecommunications pp 159–182Cite as

Compile-Time Security Certification of Imperative Programming Languages

  • Conference paper
  • First Online:

Part of the book series: Communications in Computer and Information Science ((CCIS,volume 1118))

Abstract

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.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

References

  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. Denning, D.E., Denning, P.J.: Certification of programs for secure information flow. CACM 20(7), 504–513 (1977)

    Article  Google Scholar 

  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)

    Article  Google Scholar 

  4. Denning, D.E.: A lattice model of secure information flow. CACM 19(5), 236–243 (1976)

    Article  MathSciNet  Google Scholar 

  5. Myers, A.C., Liskov, B.: Protecting privacy using the decentralized label model. ACM TOSEM 9(4), 410–442 (2000)

    Article  Google Scholar 

  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. Myers, A.C., Zheng, L., Zdancewic, S., Chong, S., Nystrom, N.: Jif: Java information flow (2001). http://www.cs.cornell.edu/jif

  8. Simonet, V., Rocquencourt, I.: Flow Caml in a nutshell. In: Proceedings of 1st APPSEM-II Workshop, pp. 152–165 (2003)

    Google Scholar 

  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. 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. Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. Sel. Areas Commun. 21(1), 5–19 (2003)

    Article  Google Scholar 

  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. Goguen, J.A., Meseguer, J.: Security policies and security models. In: IEEE Symposium on SP, p. 11 (1982)

    Google Scholar 

  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. 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. Zheng, L., Myers, A.C.: Dynamic security labels and static information flow control. Int. J. Inf. Secur. 6(2–3), 67–84 (2007)

    Article  Google Scholar 

  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)

    Article  Google Scholar 

  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)

    Article  Google Scholar 

  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). https://doi.org/10.1007/978-3-319-03542-0_16

    Chapter  MATH  Google Scholar 

  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)

    Article  MathSciNet  Google Scholar 

  21. Robling Denning, D.E.: Cryptography and Data Security. Addison-Wesley Longman Publishing Co., Boston (1982)

    MATH  Google Scholar 

  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. 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. 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. 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). https://doi.org/10.1007/978-3-642-54792-8_9

    Chapter  Google Scholar 

  26. Barnes, J.G.P.: High Integrity Software: The Spark Approach to Safety and Security. Pearson Education, London (2003)

    Google Scholar 

  27. Zdancewic, S., Zheng, L., Nystrom, N., Myers, A.C.: Secure program partitioning. ACM Trans. Comput. Syst. (TOCS) 20(3), 283–328 (2002)

    Article  Google Scholar 

  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. 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. 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. Cheng, W., et al.: Abstractions for usable information flow control in Aeolus. In: USENIX Annual Technical Conference, pp. 139–151 (2012)

    Google Scholar 

  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. 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. Hunt, S., Sands, D.: On flow-sensitive security types. ACM SIGPLAN Not. 41, 79–90 (2006)

    Article  Google Scholar 

  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. 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)

    Article  Google Scholar 

  37. Denning, D.E.R.: Secure information flow in computer systems (1975)

    Google Scholar 

Download references

Acknowledgements

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.

Author information

Authors and Affiliations

  1. Department of Computer Science and Engineering, Indian Institute of Technology Bombay, Mumbai, 400076, India

    Sandip Ghosal & R. K. Shyamasundar

  2. Institute for Development and Research in Banking Technology, Hyderabad, India

    N. V. Narendra Kumar

Authors
  1. Sandip Ghosal
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. R. K. Shyamasundar
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. N. V. Narendra Kumar
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Sandip Ghosal .

Editor information

Editors and Affiliations

  1. University of Jordan, Amman, Jordan

    Mohammad S. Obaidat

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Ghosal, S., Shyamasundar, R.K., Narendra Kumar, N.V. (2019). Compile-Time Security Certification of Imperative Programming Languages. In: Obaidat, M. (eds) E-Business and Telecommunications. ICETE 2018. Communications in Computer and Information Science, vol 1118. Springer, Cham. https://doi.org/10.1007/978-3-030-34866-3_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-34866-3_8

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-34865-6

  • Online ISBN: 978-3-030-34866-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation