Abstract
Modern optimizing compilers use the single static assignment (SSA) format for programs, as it simplifies program analysis and transformation. A source program is converted to an equivalent SSA form before it is optimized. The conversion may, however, create a less secure program if fresh SSA variables inadvertently leak sensitive values that are masked in the original program. This work defines a mechanism to restore a program to its original security level after it has been converted to SSA form and modified further by a series of optimizing transformations. The final program is converted out of SSA form by grouping variables together in a manner that blocks any new leak introduced by the initial SSA conversion. The grouping relies on taint and leakage information about the original program, which is propagated through the optimizing transformations using refinement proofs.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Static single assignment book. http://ssabook.gforge.inria.fr/latest/book.pdf
Askarov, A., Chong, S.: Learning is change in knowledge: knowledge-based security for dynamic policies. In: Chong, S. (ed.) 25th IEEE Computer Security Foundations Symposium, CSF 2012, Cambridge, MA, USA, 25–27 June 2012, pp. 308–322. IEEE Computer Society (2012)
Bell, D., LaPadula, L.: Secure computer systems: mathematical foundations, vol. 1-III. Technical report ESD-TR-73-278, The MITRE Corporation (1973). 17
Cooper, K.D., Simpson, L.T.: Live range splitting in a graph coloring register allocator. In: Koskimies, K. (ed.) CC 1998. LNCS, vol. 1383, pp. 174–187. Springer, Heidelberg (1998). doi:10.1007/BFb0026430
Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Efficiently computing static single assignment form and the control dependence graph. ACM Trans. Program. Lang. Syst. 13(4), 451–490 (1991)
Deng, C., Namjoshi, K.S.: Securing a compiler transformation. In: Rival, X. (ed.) SAS 2016. LNCS, vol. 9837, pp. 170–188. Springer, Heidelberg (2016). doi:10.1007/978-3-662-53413-7_9
Denning, D.E., Denning, P.J.: Certification of programs for secure information flow. Commun. ACM 20(7), 504–513 (1977)
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)
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)
Hack, S.: Interference graphs of programs in SSA form. Technical report 2005–15, Universität Karlsruhe, June 2005
Le, V., Afshari, M., Su, Z.: Compiler validation via equivalence modulo inputs. In: O’Boyle, M.F.P., Pingali, K. (eds.) ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2014, Edinburgh, UK, 09–11 June 2014, pp. 216–226. ACM (2014)
Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009)
Patrignani, M., Garg, D.: Secure compilation and hyperproperty preservation. In: CSF (2017, to appear)
Pereira, F.M.Q., Palsberg, J.: SSA elimination after register allocation. In: Moor, O., Schwartzbach, M.I. (eds.) CC 2009. LNCS, vol. 5501, pp. 158–173. Springer, Heidelberg (2009). doi:10.1007/978-3-642-00722-4_12
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)
Rideau, S., Leroy, X.: Validating register allocation and spilling. In: Gupta, R. (ed.) CC 2010. LNCS, vol. 6011, pp. 224–243. Springer, Heidelberg (2010). doi:10.1007/978-3-642-11970-5_13
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)
Sreedhar, V.C., Gao, G.R.: A linear time algorithm for placing phi-nodes. In: Cytron, R.K., Lee, P. (eds.) Conference Record of POPL 1995: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Francisco, California, USA, 23–25 January 1995, pp. 62–73. ACM Press (1995)
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)
Yang, X., Chen, Y., Eide, E., Regehr, J.: Finding and understanding bugs in C compilers. In: Hall, M.W., Padua, D.A. (eds.) Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, San Jose, CA, USA, 4–8 June 2011, pp. 283–294. ACM (2011)
Acknowledgements
Kedar Namjoshi was supported, in part, by grant CCF-1563393 from the National Science Foundation. We thank our colleagues at Bell Labs and UIC for helpful comments on this work.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Deng, C., Namjoshi, K.S. (2017). Securing the SSA Transform. In: Ranzato, F. (eds) Static Analysis. SAS 2017. Lecture Notes in Computer Science(), vol 10422. Springer, Cham. https://doi.org/10.1007/978-3-319-66706-5_5
Download citation
DOI: https://doi.org/10.1007/978-3-319-66706-5_5
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-66705-8
Online ISBN: 978-3-319-66706-5
eBook Packages: Computer ScienceComputer Science (R0)