Abstract
We introduce an abstract domain for information-flow analysis of software. The proposal combines variable dependency analysis with numerical abstractions, yielding to accuracy and efficiency improvements. We apply the full power of the proposal to the case of database query languages as well. Finally, we present an implementation of the analysis, called \(\mathsf {Sails}\), as an instance of a generic static analyzer. Keeping the modular construction of the analysis, the tool allows one to tune the granularity of heap analysis and to choose the numerical domain involved in the reduced product. This way the user can tune the information leakage analysis at different levels of precision and efficiency.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
- 2.
- 3.
In the rest of the paper, we will omit the initial and final labels of statements when not required.
- 4.
For other type of variables, the abstraction function represents identity function.
- 5.
Notice that, as in [45], we assume that the attacker, in both cases, knows the source code of the program.
References
Andersen, H.R.: An introduction to binary decision diagrams. Technical report, Course Notes on the WWW (1997)
Armstrong, T., Marriott, K., Schachte, P., Søndergaard, H.: Two classes of boolean functions for dependency analysis. Sci. Comput. Program. 31, 3–45 (1998)
Askarov, A., Hedin, D., Sabelfeld, A.: Cryptographically-masked flows. Theor. Comput. Sci. 402, 82–101 (2008)
Askarov, A., Sabelfeld, A.: Security-typed languages for implementation of cryptographic protocols: a case study. In: di Vimercati, S.C., Syverson, P., Gollmann, D. (eds.) ESORICS 2005. LNCS, vol. 3679, pp. 197–221. Springer, Heidelberg (2005). https://doi.org/10.1007/11555827_12
Bagnara, R., Hill, P.M., Zaffanella, E.: The parma polyhedra library: toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci. Comput. Program. 72, 3–21 (2008)
Bagnara, R., Hill, P.M., Zaffanella, E.: Applications of polyhedral computations to the analysis and verification of hardware and software systems. Theor. Comput. Sci. 410, 4672–4691 (2009)
Banerjee, A., Naumann, D.A.: Secure information flow and pointer confinement in a Java-like language. In: Proceedings of the 15th IEEE Workshop on Computer Security Foundations, CSFW 2002. IEEE Computer Society, Washington, DC (2002)
Barthe, G., Rezk, T.: Non-interference for a JVM-like language. In: Proceedings of the 2005 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, TLDI 2005, pp. 103–112. ACM, New York (2005)
Bodei, C., Degano, P., Nielson, F., Nielson, H.R.: Static analysis for secrecy and non-interference in networks of processes. In: Malyshkin, V. (ed.) PaCT 2001. LNCS, vol. 2127, pp. 27–41. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-44743-1_3
Clause, J., Li, W., Orso, A.: Dytan: a generic dynamic taint analysis framework. In: Proceedings of the 2007 International Symposium on Software Testing and Analysis, ISSTA 2007, pp. 196–206. ACM, New York (2007)
Cortesi, A., Filé, G., Winsborough, W.H.: Prop revisited: propositional formula as abstract domain for groundness analysis. In: LICS, pp. 322–327 (1991)
Costantini, G., Ferrara, P., Cortesi, A.: Static analysis of string values. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 505–521. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-24559-6_34
Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL 1979, pp. 269–282. ACM, New York (1979)
Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proceedings of the 5th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL 1978, pp. 84–96. ACM, New York (1978)
De Groef, W., Devriese, D., Nikiforakis, N., Piessens, F.: FlowFox: a web browser with flexible and precise information flow control. In: Proceedings of the 19th ACM Conference on Computer and Communications Security (CCS 2012). ACM (2012)
Denning, D.E.: A lattice model of secure information flow. Commun. ACM 19, 236–243 (1976)
Denning, D.E., Denning, P.J.: Certification of programs for secure information flow. Commun. ACM 20, 504–513 (1977)
Ferrara, P.: Static type analysis of pattern matching by abstract interpretation. In: Hatcliff, J., Zucca, E. (eds.) FMOODS/FORTE-2010. LNCS, vol. 6117, pp. 186–200. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-13464-7_15
Ferrara, P.: A fast and precise alias analysis for data race detection. In: Proceedings of the Third Workshop on Bytecode Semantics, Verification, Analysis and Transformation (Bytecode 2008), Electronic Notes in Theoretical Computer Science. Elsevier, April 2008
Focardi, R., Centenaro, M.: Information flow security of multi-threaded distributed programs. In: Proceedings of the third ACM SIGPLAN Workshop on Programming Languages and Analysis for Security, PLAS 2008, pp. 113–124. ACM, New York (2008)
Giacobazzi, R., Mastroeni, I.: Abstract non-interference: parameterizing non-interference by abstract interpretation. In: Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004, pp. 186–197. ACM, New York (2004)
Halder, R., Cortesi, A.: Abstract interpretation of database query languages. Comput. Lang. Syst. Struct. 38, 123–157 (2012)
Halder, R., Cortesi, A.: Abstract program slicing of database query languages. In: Proceedings of the 28th Annual ACM Symposium on Applied Computing, Coimbra, Portugal, pp. 838–845. ACM Press (2013)
Halder, R., Zanioli, M., Cortesi, A.: Information leakage analysis of database query languages. In: Proceedings of the 29th Annual ACM Symposium on Applied Computing, Gyeongju, Korea, pp. 813–820. ACM Press, 24–28 March 2014
Hennessy, M.: The Semantics of Programming Languages: An Elementary Introduction Using Structural Operational Semantics. Wiley, New York (1990)
Jeannet, B.: Convex polyhedra library, March 2002. Documentation of the “New Polka” library. http://www.irisa.fr/prive/Bertrand.Jeannet/newpolka.html
Jeannet, B., Miné, A.: Apron: a library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 661–667. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02658-4_52
Joshi, R., Rustan, K., Leino, M.: A semantic approach to secure information flow. Sci. Comput. Program. 37, 113–138 (2000)
Laud, P.: Semantics and program analysis of computationally secure information flow. In: Sands, D. (ed.) ESOP 2001. LNCS, vol. 2028, pp. 77–91. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45309-1_6
Liu, J.D., George, M.D., Vikram, K., Qi, X., Waye, L., Myers, A.C.: Fabric: a platform for secure distributed computation and storage. In: Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles, SOSP 2009, pp. 321–334. ACM, New York (2009)
Liu, Y., Milanova, A.: Static information flow analysis with handling of implicit flows and a study on effects of implicit flows vs explicit flows. In: Proceedings of the 2010 14th European Conference on Software Maintenance and Reengineering, CSMR 2010, pp. 146–155. IEEE Computer Society, Washington, DC (2010)
Miné, A.: A new numerical abstract domain based on difference-bound matrices. In: Danvy, O., Filinski, A. (eds.) PADO 2001. LNCS, vol. 2053, pp. 155–172. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-44978-7_10
Miné, A.: The octagon abstract domain. In: Proceedings of the Workshop on Analysis, Slicing, and Transformation (AST 2001), pp. 310–319. IEEE CS Press, October 2001
Myers, A.C., Zheng, L., Zdancewic, S., Chong, S., Nystrom, N.: JIF: Java information flow. Software release, July 2001–2004
Pottier, F., Simonet, V.: Information flow inference for ML. ACM Trans. Program. Lang. Syst. 25, 117–158 (2003)
Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. Sel. Areas Commun. 21(1), 5–19 (2003)
Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst. 24, 217–298 (2002)
Simonet, V.: The flow Caml System: documentation and user’s manual. Technical report 0282, Institut National de Recherche en Informatique et en Automatique (INRIA), July 2003
Smith, G.: Principles of secure information flow analysis. In: Malware Detection, pp. 297–307 (2007)
Smith, G., Volpano, D.: Secure information flow in a multi-threaded imperative language. In: Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1998, pp. 355–364. ACM, New York (1998)
Stefan, D., Russo, A., Mitchell, J.C., Mazières, D.: Flexible dynamic information flow control in Haskell. SIGPLAN Not. 46(12), 95–106 (2011)
Tolstrup, T.K., Nielson, F., Nielson, H.R.: Information flow analysis for VHDL. In: Malyshkin, V. (ed.) PaCT 2005. LNCS, vol. 3606, pp. 79–98. Springer, Heidelberg (2005). https://doi.org/10.1007/11535294_8
Stanford University. Stanford SecuriBench Micro. http://suif.stanford.edu/~livshits/work/securibench-micro/
Volpano, D., Irvine, C., Smith, G.: A sound type system for secure flow analysis. J. Comput. Secur. 4, 167–187 (1996)
Zanioli, M., Cortesi, A.: Information leakage analysis by abstract interpretation. In: Černá, I., Gyimóthy, T., Hromkovič, J., Jefferey, K., Králović, R., Vukolić, M., Wolf, S. (eds.) SOFSEM 2011. LNCS, vol. 6543, pp. 545–557. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-18381-2_45
Zanioli, M., Ferrara, P., Cortesi, A.: Sails: static analysis of information leakage with sample. In: Proceedings of the 2012 ACM Symposium on Applied Computing, pp. 1308–1313. ACM Press (2012)
Zanotti, M.: Security typings by abstract interpretation. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 360–375. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45789-5_26
Acknowledgments
This work has been partially supported by CINI Cybersecurity National Laboratory within the project “FilieraSicura: Securing the Supply Chain of Domestic Critical Infrastructures from Cyber Attacks” funded by CISCO Systems Inc. and Leonardo SpA, and by MIUR-MAE within the Project “Formal Specification for Secured Software System”, under the Indo-Italian Executive Programme of Cooperation in Scientific and Technological Cooperation Project number IN17MO07.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer-Verlag GmbH Germany
About this chapter
Cite this chapter
Cortesi, A., Ferrara, P., Halder, R., Zanioli, M. (2018). Combining Symbolic and Numerical Domains for Information Leakage Analysis. In: Gavrilova, M., Tan, C., Chaki, N., Saeed, K. (eds) Transactions on Computational Science XXXI. Lecture Notes in Computer Science(), vol 10730. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-56499-8_6
Download citation
DOI: https://doi.org/10.1007/978-3-662-56499-8_6
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-56498-1
Online ISBN: 978-3-662-56499-8
eBook Packages: Computer ScienceComputer Science (R0)