Information Leakage in Arbiter Protocols

  • Nestan TsiskaridzeEmail author
  • Lucas Bang
  • Joseph McMahan
  • Tevfik Bultan
  • Timothy Sherwood
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11138)


Resource sharing while preserving privacy is an increasingly important problem due to a wide-scale adoption of cloud computing. Under multitenancy, it is common to have multiple mutually distrustful “processes” (e.g. cores, threads, etc.) running on the same system simultaneously. This paper explores a new approach for automatically identifying and quantifying the information leakage in protocols that arbitrate utilization of shared resources between processes. Our approach is based on symbolic execution of arbiter protocols to extract constraints relating adversary observations to victim requests, then using model counting constraint solvers to quantify the information leaked. We present enumerative and optimized methods of exact model counting, and apply our methods to a set of nine different arbiter protocols, quantifying their leakage under different scenarios and allowing for informed comparison.


Arbiter protocols Quantitative information flow Model counting Symbolic execution 


  1. 1.
    Aydin, A., Bang, L., Bultan, T.: Automata-based model counting for string constraints. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015, Part I. LNCS, vol. 9206, pp. 255–272. Springer, Cham (2015). Scholar
  2. 2.
    Backes, M., Kopf, B., Rybalchenko, A.: Automatic discovery and quantification of information leaks. In: Proceedings of the 30th IEEE Symposium on Security and Privacy, SP 2009, Washington, DC, USA (2009)Google Scholar
  3. 3.
    Backes, M., Pfitzmann, B.: Computational probabilistic noninterference. Int. J. Inf. Sec. 3(1), 42–60 (2004)CrossRefGoogle Scholar
  4. 4.
    Cabuk, S., Brodley, C.E., Shields, C.: IP covert channel detection. ACM Trans. Inf. Syst. Secur. 12(4), 22:1–22:29 (2009)CrossRefGoogle Scholar
  5. 5.
    Chothia, T., Kawamoto, Y., Novakovic, C.: Leakwatch: estimating information leakage from java programs. In: Proceedings of 19th European Symposium on Research in Computer Security, Computer Security - ESORICS 2014 (2014)Google Scholar
  6. 6.
    Clark, D., Hunt, S., Malacaria, P.: A static analysis for quantifying information flow in a simple imperative language. J. Comput. Secur. 15(3), 321–371 (2007)CrossRefGoogle Scholar
  7. 7.
    Ensafi, R., Park, J.C., Kapur, D., Crandall, J.R.: Idle port scanning and non-interference analysis of network protocol stacks using model checking. In: 19th USENIX Security Symposium, Washington, DC, USA (2010)Google Scholar
  8. 8.
    Ferraiuolo, A., Hua, W., Myers, A.C., Suh, G.E.: Secure information flow verification with mutable dependent types. In: Proceedings of the 54th Annual Design Automation Conference, DAC 2017 (2017)Google Scholar
  9. 9.
    Gong, X., Kiyavash, A.: Quantifying the information leakage in timing side channels in deterministic work-conserving schedulers. IEEE/ACM Trans. Netw. 24(3), 1841–1852 (2016)CrossRefGoogle Scholar
  10. 10.
    Guo, S., Wu, M., Wang, C.: Symbolic execution of programmable logic controller code. In: ESEC/SIGSOFT FSE (2017)Google Scholar
  11. 11.
    Gupta, J., Goel, N.: Efficient bus arbitration protocol for SoC design. In: 2015 International Conference on Smart Technologies and Management for Computing, Communication, Controls, Energy and Materials (ICSTM) (2015)Google Scholar
  12. 12.
    Heusser, J., Malacaria, P.: Quantifying information leaks in software. In: Twenty-Sixth Annual Computer Security Applications Conference, ACSAC 2010, Austin, Texas, USA, 6–10 December 2010, pp. 261–269 (2010)Google Scholar
  13. 13.
    Hughes, D.J.D., Shmatikov, V.: Information hiding, anonymity and privacy: a modular approach. J. Comput. Secur. 12(1), 3–36 (2004)CrossRefGoogle Scholar
  14. 14.
    Kadloor, S., Kiyavash, N.: Delay optimal policies offer very little privacy. In: Proceedings of the IEEE INFOCOM 2013, Turin, Italy (2013)Google Scholar
  15. 15.
    Klebanov, V., Manthey, N., Muise, C.: SAT-based analysis and quantification of information flow in programs. In: Joshi, K., Siegle, M., Stoelinga, M., D’Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054. Springer, Heidelberg (2013). Scholar
  16. 16.
    Köpf, B., Basin, D.A.: An information-theoretic model for adaptive side-channel attacks. In: Proceedings of the ACM Conference on Computer and Communications Security, CCS 2007, Alexandria, Virginia, USA (2007)Google Scholar
  17. 17.
    De Loera, J.A., Hemmecke, R., Tauzer, J., Yoshida, R.: Effective lattice point counting in rational convex polytopes. J. Symb. Comput. 38(4), 1273–1302 (2004)MathSciNetCrossRefGoogle Scholar
  18. 18.
    Malacaria, P., Khouzani, M.H.R., Pasareanu, C.S., Phan, Q.S., Luckow, K.: Symbolic side-channel analysis for probabilistic programs. IACR Cryptology ePrint Archive, 2018, p. 329 (2018)Google Scholar
  19. 19.
    McCamant, S., Ernst, M.D.: Quantitative information flow as network flow capacity. In: Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, Tucson, AZ, USA (2008)Google Scholar
  20. 20.
    Phan, Q.S., Bang, L., Pasareanu, C.S., Malacaria, P., Bultan, T.: Synthesis of adaptive side-channel attacks. In: 30th IEEE Computer Security Foundations Symposium, CSF 2017, Santa Barbara, CA, USA (2017)Google Scholar
  21. 21.
    Phan, Q.-S., Malacaria, P., Tkachuk, O., Pasareanu, C.S.: Symbolic quantitative information flow. ACM SIGSOFT Softw. Eng. Notes 37(6), 1–5 (2012)CrossRefGoogle Scholar
  22. 22.
    Păsăreanu, C.S., Phan, Q.S., Malacaria, P.: Multi-run side-channel analysis using Symbolic Execution and Max-SMT. In: 29th IEEE Computer Security Foundations Symposium, CSF 2016, Washington, DC, USA (2016)Google Scholar
  23. 23.
    Păsăreanu, C.S., Visser, W., Bushnell, D., Geldenhuys, J., Mehlitz, P., Rungta, N.: Symbolic PathFinder: integrating symbolic execution with model checking for Java bytecode analysis. ASE 20, 391 (2013)Google Scholar
  24. 24.
    Sellke, S.H., Wang, C.C., Shroff, N.E., Bagchi, S.: Capacity bounds on timing channels with bounded service times. In: 2007 IEEE International Symposium on Information Theory, pp. 981–985 (2007)Google Scholar
  25. 25.
    Smith, G.: On the foundations of quantitative information flow. In: Proceedings of the 12th International Conference on Foundations of Software Science and Computational Structures (FOSSACS), pp. 288–302 (2009)CrossRefGoogle Scholar
  26. 26.
    Wang, C., Patrick, S.: Security by compilation: an automated approach to comprehensive side-channel resistance. ACM SIGLOG News 4(2), 76–89 (2017)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  • Nestan Tsiskaridze
    • 1
    Email author
  • Lucas Bang
    • 2
  • Joseph McMahan
    • 1
  • Tevfik Bultan
    • 1
  • Timothy Sherwood
    • 1
  1. 1.University of CaliforniaSanta BarbaraUSA
  2. 2.Harvey Mudd CollegeClaremontUSA

Personalised recommendations