Synthesis of a Permissive Security Monitor

  • Narges KhakpourEmail author
  • Charilaos Skandylas
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11098)


In this paper, we propose a new sound method to synthesize a permissive monitor using boolean supervisory controller synthesis that observes a Java program at certain checkpoints, predicts information flow violations and applies suitable countermeasures to prevent violations. To improve the permissiveness, we train the monitor and remove false positives by executing the program along with its executable model. If a security violation is detected, the user can define sound countermeasures, including declassification to apply in the checkpoints. We implement a tool that automates the whole process and generates a monitor. We evaluate our method by applying it on the Droidbench benchmark and one real-life Android application.


  1. 1.
  2. 2.
    Askarov, A., Sabelfeld, A.: Localized delimited release: combining the what and where dimensions of information release. In: Proceedings of the 2007 Workshop on Programming Languages and Analysis for Security, PLAS 2007, San Diego, California, USA, 14 June 2007, pp. 53–60 (2007)Google Scholar
  3. 3.
    Austin, T.H., Flanagan, C.: Efficient purely-dynamic information flow analysis. In: Proceedings of the ACM SIGPLAN Fourth Workshop on Programming Languages and Analysis for Security, PLAS 2009, New York, NY, USA, pp. 113–124 (2009)Google Scholar
  4. 4.
    Austin, T.H., Flanagan, C.: Permissive dynamic information flow analysis. In: Proceedings of the 5th ACM SIGPLAN Workshop on Programming Languages and Analysis for Security, PLAS 2010, New York, NY, USA, pp. 3:1–3:12. ACM, New York (2010)Google Scholar
  5. 5.
    Austin, T.H., Flanagan, C.: Multiple facets for dynamic information flow. In: Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, New York, NY, USA, pp. 165–178. ACM, New York (2012)Google Scholar
  6. 6.
    Berthier, N., Marchand, H.: Discrete controller synthesis for infinite state systems with ReaX. In: 12th International Workshop on Discrete Event Systems, WODES 2014, Cachan, France, 14–16 May 2014, pp. 46–53 (2014)Google Scholar
  7. 7.
    Besson, F., Bielova, N., Jensen, T.P.: Hybrid information flow monitoring against web tracking. In: 2013 IEEE 26th Computer Security Foundations Symposium, New Orleans, LA, USA, 26–28 June 2013, pp. 240–254 (2013)Google Scholar
  8. 8.
    Bielova, N., Rezk, T.: A taxonomy of information flow monitors. In: Piessens, F., Viganò, L. (eds.) POST 2016. LNCS, vol. 9635, pp. 46–67. Springer, Heidelberg (2016). Scholar
  9. 9.
    Dam, M., Le Guernic, G., Lundblad, A.: TreeDroid: a tree automaton based approach to enforcing data processing policies. In: Proceedings of the 2012 ACM Conference on Computer and Communications Security, CCS 2012, New York, NY, USA, pp. 894–905. ACM, New York (2012)Google Scholar
  10. 10.
    Denning, D.E., Denning, P.J.: Certification of programs for secure information flow. Commun. ACM 20(7), 504–513 (1977)CrossRefGoogle Scholar
  11. 11.
    Devriese, D., Piessens, F.: Noninterference through secure multi-execution. In: 31st IEEE Symposium on Security and Privacy, S&P 2010, Berleley/Oakland, California, USA, 16–19 May 2010, pp. 109–124 (2010)Google Scholar
  12. 12.
    Desharnais, J., Kozyri, E., Tawbi, N.: Block-safe information flow control. Technical report, Cornell University (2016)Google Scholar
  13. 13.
    Goguen, J.A., Meseguer, J.: Security policies and security models. In: 1982 IEEE Symposium on Security and Privacy, Oakland, CA, USA, 26–28 April 1982, pp. 11–20 (1982)Google Scholar
  14. 14.
    Le Guernic, G., Banerjee, A., Jensen, T., Schmidt, D.A.: Automata-based confidentiality monitoring. In: Okada, M., Satoh, I. (eds.) ASIAN 2006. LNCS, vol. 4435, pp. 75–89. Springer, Heidelberg (2007). Scholar
  15. 15.
    Hedin, D., Sabelfeld, A.: Information-flow security for a core of JavaScript. In: 25th IEEE Computer Security Foundations Symposium, CSF 2012, Cambridge, MA, USA, 25–27 June 2012, pp. 3–18 (2012)Google Scholar
  16. 16.
    Khakpour, N., Skandylas, C.: Symbolic synthesis of a permissive security monitor: the extended version. Technical report, Linnaeus University (2018)Google Scholar
  17. 17.
    Kwon, Y., et al.: LDX: causality inference by lightweight dual execution. In: Proceedings of the Twenty-First International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2016, New York, NY, USA, pp. 503–515. ACM, New York (2016)Google Scholar
  18. 18.
    Le Guernic, G.: Confidentiality enforcement using dynamic information flow analyses. Ph.D. thesis, Manhattan, KS, USA (2007)Google Scholar
  19. 19.
    Pullicino, K.: Jif: language-based information-flow security in Java. CoRR, abs/1412.8639 (2014)Google Scholar
  20. 20.
    Russo, A., Sabelfeld, A.: Dynamic vs. static flow-sensitive security analysis. In: Proceedings of the 23rd IEEE Computer Security Foundations Symposium, CSF 2010, Edinburgh, United Kingdom, 17–19 July 2010, pp. 186–199 (2010)Google Scholar
  21. 21.
    Sabelfeld, A., Russo, A.: From dynamic to static and back: riding the roller coaster of information-flow control research. In: Pnueli, A., Virbitskaite, I., Voronkov, A. (eds.) PSI 2009. LNCS, vol. 5947, pp. 352–365. Springer, Heidelberg (2010). Scholar
  22. 22.
    Santos, J.F., Rezk, T.: An information flow monitor-inlining compiler for securing a core of JavaScript. In: Proceedings of the ICT Systems Security and Privacy Protection - 29th IFIP TC 11 International Conference, SEC 2014, Marrakech, Morocco, 2–4 June 2014, pp. 278–292 (2014)Google Scholar
  23. 23.
    Schoepe, D., Balliu, M., Pierce, B.C., Sabelfeld, A.: Explicit secrecy: a policy for taint tracking. In: IEEE European Symposium on Security and Privacy, Euro S&P 2016, Saarbrücken, Germany, 21–24 March 2016, pp. 15–30 (2016)Google Scholar
  24. 24.
    Shroff, P., Smith, S., Thober, M.: Dynamic dependency monitoring to secure information flow. In: 20th IEEE Computer Security Foundations Symposium (CSF 2007), Venice, Italy, 6–8 July 2007, pp. 203–217, July 2007Google Scholar
  25. 25.
    Simonet, V.: The flow caml system. Software release, vol. 116, pp. 119–156 (2003).
  26. 26.
    Zdancewic, S.A.: Programming languages for information security. Ph.D. thesis, Ithaca, NY, USA (2002)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.Linnaeus UniversityVäxjöSweden

Personalised recommendations