Skip to main content
SpringerLink
Log in
Book cover

International Static Analysis Symposium

SAS 2016: Static Analysis pp 170–188Cite as

Securing a Compiler Transformation

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 9837))

Abstract

A compiler can be correct and yet be insecure. That is, a compiled program may have the same input-output behavior as the original, and yet leak more information. An example is the commonly applied optimization which removes dead (i.e., useless) stores. It is shown that deciding a posteriori whether a new leak has been introduced as a result of eliminating dead stores is difficult: it is PSPACE-hard for finite-state programs and undecidable in general. In contrast, deciding the correctness of dead store removal is in polynomial time. In response to the hardness result, a sound but approximate polynomial-time algorithm for secure dead store elimination is presented and proved correct. Furthermore, it is shown that for several other compiler transformations, security follows from correctness.

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. Abadi, M.: Protection in programming-language translations. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 868–883. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  2. de Amorim, A.A., Collins, N., DeHon, A., Demange, D., Hritcu, C., Pichardie, D., Pierce, B.C., Pollack, R., Tolmach, A.: A verified information-flow architecture. In: Jagannathan, S., Sewell, P. (eds.) The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014, San Diego, CA, USA, 20–21 January 2014, pp. 165–178. ACM (2014). http://doi.acm.org/10.1145/2535838.2535839

  3. Bell, D., LaPadula, L.: Secure computer systems: Mathematical foundations, vol. 1-III. Technical report ESD-TR-73-278, The MITRE Corporation (1973)

    Google Scholar 

  4. Ceara, D., Mounier, L., Potet, M.: Taint dependency sequences: a characterization of insecure execution paths based on input-sensitive cause sequences. In: Third International Conference on Software Testing, Verification and Validation, ICST 2010, Paris, France, 7–9 April 2010. Workshops Proceedings, pp. 371–380 (2010). http://dx.doi.org/10.1109/ICSTW.2010.28

  5. Denning, D.E.: Secure information flow in computer systems. Ph.D. thesis, Purdue University, May 1975

    Google Scholar 

  6. Denning, D.E., Denning, P.J.: Certification of programs for secure information flow. Commun. ACM 20(7), 504–513 (1977). http://doi.acm.org/10.1145/359636.359712

    Article  MATH  Google Scholar 

  7. D’Silva, V., Payer, M., Song, D.X.: The correctness-security gap in compiler optimization. In: 2015 IEEE Symposium on Security and Privacy Workshops, SPW 2015, San Jose, CA, USA, 21–22 May 2015, pp. 73–87. IEEE Computer Society (2015). http://dx.doi.org/10.1109/SPW.2015.33

  8. Fournet, C., Swamy, N., Chen, J., Dagand, P., Strub, P., Livshits, B.: Fully abstract compilation to JavaScript. In: Giacobazzi, R., Cousot, R. (eds.) The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2013, Rome, Italy, 23–25 January 2013, pp. 371–384. ACM (2013). http://doi.acm.org/10.1145/2429069.2429114

  9. Gondi, K., Bisht, P., Venkatachari, P., Sistla, A.P., Venkatakrishnan, V.N.: SWIPE: eager erasure of sensitive data in large scale systems software. In: Bertino, E., Sandhu, R.S. (eds.) Second ACM Conference on Data and Application Security and Privacy, CODASPY 2012, San Antonio, TX, USA, 7–9 February 2012, pp. 295–306. ACM (2012). http://doi.acm.org/10.1145/2133601.2133638

  10. Howard, M.: When scrubbing secrets in memory doesn’t work (2002). http://archive.cert.uni-stuttgart.de/bugtraq/2002/11/msg00046.html. Also https://cwe.mitre.org/data/definitions/14.html

  11. Namjoshi, K.S., Zuck, L.D.: Witnessing program transformations. In: Logozzo, F., Fähndrich, M. (eds.) Static Analysis. LNCS, vol. 7935, pp. 304–323. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  12. Necula, G.: Translation validation of an optimizing compiler. In: Proceedings of the ACM SIGPLAN Conference on Principles of Programming Languages Design and Implementation (PLDI 2000), pp. 83–95 (2000)

    Google Scholar 

  13. Papadimitriou, C.H.: Computational Complexity. Addison-Wesley, Reading (1994)

    MATH  Google Scholar 

  14. Patrignani, M., Agten, P., Strackx, R., Jacobs, B., Clarke, D., Piessens, F.: Secure compilation to protected module architectures. ACM Trans. Program. Lang. Syst. 37(2), 6 (2015). http://doi.acm.org/10.1145/2699503

    Google Scholar 

  15. Pnueli, A., Shtrichman, O., Siegel, M.: The code validation tool (CVT)- automatic verification of a compilation process. Softw. Tools Technol. Transf. 2(2), 192–201 (1998)

    Article  MATH  Google Scholar 

  16. Smith, G.: Recent developments in quantitative information flow (invited tutorial). In: 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, 6–10 July 2015, pp. 23–31. IEEE (2015). http://dx.doi.org/10.1109/LICS.2015.13

  17. 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). http://dx.doi.org/10.3233/JCS-1996-42-304

    Article  Google Scholar 

  18. Zuck, L.D., Pnueli, A., Goldberg, B.: VOC: a methodology for the translation validation of optimizing compilers. J. UCS 9(3), 223–247 (2003)

    Google Scholar 

Download references

Acknowledgements

We would like to thank Lenore Zuck, V.N. Venkatakrishnan and Sanjiva Prasad for helpful discussions and comments on this research. This work was supported, in part, by DARPA under agreement number FA8750-12-C-0166. The U.S. Government is authorized to reproduce and distribute reprints for Governmental purposes notwithstanding any copyright notation thereon. The views and conclusions contained herein are those of the authors and should not be interpreted as necessarily representing the official policies or endorsements, either expressed or implied, of DARPA or the U.S. Government.

Author information

Authors and Affiliations

  1. New York University, New York City, USA

    Chaoqiang Deng

  2. Bell Laboratories, Nokia, Murray Hill, USA

    Kedar S. Namjoshi

Authors
  1. Chaoqiang Deng
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Kedar S. Namjoshi
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Kedar S. Namjoshi .

Editor information

Editors and Affiliations

  1. Ecole Normale Supérieure , Paris, France

    Xavier Rival

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer-Verlag GmbH Germany

About this paper

Cite this paper

Deng, C., Namjoshi, K.S. (2016). Securing a Compiler Transformation. In: Rival, X. (eds) Static Analysis. SAS 2016. Lecture Notes in Computer Science(), vol 9837. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-53413-7_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-662-53413-7_9

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-662-53412-0

  • Online ISBN: 978-3-662-53413-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation