Bernd Finkbeiner
ABSTRACT
We consider the automatic verification of information flow security policies of web-based workflows, such as conference submission systems like EasyChair. Our workflow description language allows for loops, non-deterministic choice, and an unbounded number of participating agents. The information flow policies are specified in a temporal logic for hyperproperties. We show that the verification problem can be reduced to the satisfiability of a formula of first-order linear-time temporal logic, and provide decidability results for relevant classes of workflows and specifications. We report on experimental results obtained with an implementation of our approach on a series of benchmarks.
Supplemental Material
- Aharon Abadi, Alexander Rabinovich, and Mooly Sagiv. 2010. Decidable fragments of many-sorted logic. Journal of Symbolic Computation 45, 2 (2010), 153-- 172. Google Scholar
Digital Library
- Myrto Arapinis, Sergiu Bursuc, and Mark Ryan. 2012. Privacy Supporting Cloud Computing: ConfiChair, a Case Study. In Proc. POST 2012. Springer Verlag, 89-- 108. Google ScholarDigital Library
- Thomas Ball, Nikolaj Bjørner, Aaron Gember, Shachar Itzhaky, Aleksandr Karbyshev, Mooly Sagiv, Michael Schapira, and Asaf Valadarsky. 2014. VeriCon: towards verifying controller programs in software-defined networks. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2014). ACM, 282--293. Google ScholarDigital Library
- Thomas Bauereiß and Dieter Hutter. 2014. Information flow control for workflow management systems. it - Information Technology 56, 6 (2014), 294--299.Google Scholar
- Thomas Bauereiß, Armando Pesenti Gritti, Andrei Popescu, and Franco Raimondi. 2017. CoSMeDis: A Distributed Social Media Platform with Formally Verified Confidentiality Guarantees. (2017). to appear in Security and Privacy 2017.Google Scholar
- Robert Berger. 1966. The undecidability of the domino problem. Number 66. American Mathematical Soc.Google Scholar
- C. Bhardwaj and S. Prasad. 2015. Parametric information flow control in ehealth. In Proceedings HealthCom 2015. 102--107. https://doi.org/10.1109/HealthCom. 2015.7454481Google Scholar
- Egon Börger, Erich Grädel, and Yuri Gurevich. 1997. The Classical Decision Problem. Springer. Google ScholarCross Ref
- Michael R Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K Micinski, Markus N Rabe, and César Sánchez. 2014. Temporal logics for hyperproperties. In International Conference on Principles of Security and Trust. Springer, 265--284.Google ScholarCross Ref
- Michael R. Clarkson and Fred B. Schneider. 2010. Hyperproperties. Journal of Computer Security 18, 6 (2010), 1157--1210. Google ScholarDigital Library
- Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: An efficient SMT solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 337--340.Google ScholarDigital Library
- Remco M Dijkman, Marlon Dumas, and Chun Ouyang. 2008. Semantics and analysis of business process models in BPMN. Information and Software technology 50, 12 (2008), 1281--1294.Google Scholar
- R. Dimitrova, B. Finkbeiner, M. Kovács, M. N. Rabe, and H. Seidl. 2012. Model Checking Information Flow in Reactive Systems. In Proc. VMCAI'12. 169--185. Google ScholarDigital Library
- R. Fagin, J. Y. Halpern, Y. Moses, and M. Y. Vardi. 1995. Reasoning About Knowledge. MIT Press.Google Scholar
- Bernd Finkbeiner and Christopher Hahn. 2016. Deciding Hyperproperties. In 27th International Conference on Concurrency Theory (CONCUR 2016) (Leibniz International Proceedings in Informatics (LIPIcs)), Josée Desharnais and Radha Jagadeesan (Eds.), Vol. 59. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 13:1--13:14.Google Scholar
- Bernd Finkbeiner, Helmut Seidl, and Christian Müller. 2016. Specifying and Verifying Secrecy in Workflows with Arbitrarily Many Agents. In Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA 2016) (Lecture Notes in Computer Science), Vol. 9938. 157--173. Google ScholarCross Ref
- J. A. Goguen and J. Meseguer. 1982. Security Policies and Security Models. In Proceedings of the IEEE Symposium on Security and Privacy. 11--20. Google ScholarCross Ref
- Ian M. Hodkinson, Frank Wolter, and Michael Zakharyaschev. 2000. Decidable fragment of first-order temporal logics. Ann. Pure Appl. Logic 106, 1--3 (2000), 85--134.Google ScholarCross Ref
- Daniel Jackson. 2012. Software Abstractions: logic, language, and analysis. MIT press.Google Scholar
- Emmanuel Jeandel. 2010. The periodic domino problem revisited. Theoretical Computer Science 411, 44--46 (2010), 4010--4016.Google ScholarCross Ref
- Sudeep Kanav, Peter Lammich, and Andrei Popescu. 2014. A Conference Management System with Verified Document Confidentiality. In Proceedings of the 26th International Conference on Computer Aided Verification (CAV 2014). Springer Verlag, 167--183.Google ScholarDigital Library
- Denis Kuperberg, Julien Brunel, and David Chemouil. 2016. On Finite Domains in First-Order Linear Temporal Logic. In International Symposium on Automated Technology for Verification and Analysis. Springer, 211--226. Google ScholarCross Ref
- Jianwen Li, Yinbo Yao, Geguang Pu, Lijun Zhang, and Jifeng He. 2014. Aalta: An LTL Satisfiability Checker over Infinite/Finite Traces. In Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE 2014). ACM, 731--734. Google ScholarDigital Library
- Nuno Macedo, Julien Brunel, David Chemouil, Alcino Cunha, and Denis Kuperberg. 2016. Lightweight specification and analysis of dynamic systems with rich configurations. In Proceedings of the 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE 2016). ACM, 373--383. Google ScholarDigital Library
- Zohar Manna and Amir Pnueli. 1981. Verification of Concurrent Programs: The Temporal Framework. In The Correctness Problem in Computer Science, Robert S. Boyer and J Strother Moore (Eds.). Academic Press, London, 215--273.Google Scholar
- Heiko Mantel. 2000. Possibilistic Definitions of Security -- An Assembly Kit. In Proceedings of the 13th IEEE Computer Security Foundations Workshop (CSFW). IEEE Computer Society, 185--199. Google ScholarCross Ref
- Timothy Nelson, Daniel J. Dougherty, Kathi Fisler, and Shriram Krishnamurthi. 2012. Toward a More Complete Alloy. In Proceedings of the 3rd International Conference on Abstract State Machines, Alloy, B, VDM, and Z (ABZ 2012) (Lecture Notes in Computer Science), Vol. 7316. Springer, 136--149. Google ScholarDigital Library
- A. Sabelfeld and D. Sands. 2005. Dimensions and Principles of Declassification. In Proceedings CSFW'05. IEEE Computer Society, 255--269. Google ScholarDigital Library
- A. P. Sistla and E. M. Clarke. 1985. The Complexity of Propositional Linear Temporal Logics. J. ACM 32, 3 (July 1985), 733--749. Google ScholarDigital Library
- David Sutherland. 1986. A model of information. In Proc. 9th National Computer Security Conference. DTIC Document, 175--183.Google Scholar
- Hao Wang. 1990. Dominoes and the AEA case of the decision problem. In Computation, Logic, Philosophy. Springer, 218--245. Google ScholarCross Ref
- Christoph Weidenbach, Dilyana Dimova, Arnaud Fietzke, Rohit Kumar, Martin Suda, and Patrick Wischnewski. 2009. SPASS Version 3.5. In International Conference on Automated Deduction. Springer, 140--145. Google ScholarDigital Library
- S. Zdancewic and A. C. Myers. 2003. Observational Determinism for Concurrent Program Security. In Proceedings of CSFW'03. Google ScholarCross Ref
Index Terms
- Verifying Security Policies in Multi-agent Workflows with Loops
Recommendations
Verifying Multi-Agent Systems by Model Checking Three-valued Abstractions
AAMAS '15: Proceedings of the 2015 International Conference on Autonomous Agents and Multiagent SystemsWe develop the theoretical foundations of a predicate abstraction methodology for the verification of multi-agent systems. We put forward a specification language based on epistemic logic and a weak variant of the logic ATL interpreted on a three-valued ...
Metareasoning for multi-agent epistemic logics
CLIMA'04: Proceedings of the 5th international conference on Computational Logic in Multi-Agent SystemsWe present an encoding of a sequent calculus for a multiagent epistemic logic in Athena, an interactive theorem proving system for many-sorted first-order logic. We then use Athena as a metalanguage in order to reason about the multi-agent logic an as ...
Comments