Stream-Monitoring Automata
Pages 313 - 320
Abstract
Over the past nearly twenty years, numerous formal models of enforcement and runtime monitors have been investigated. This paper takes the lessons learned from earlier models and proffers a new general model of runtime enforcement that is more suitable for modeling security mechanisms that operate over infinite event streams. The new model, called Stream-Monitoring Automata (SMAs), enables the constraints and analyses of interest in previous models to be encoded, and overcomes several shortcomings of existing models with respect to expressiveness. SMAs capture the practical abilities of mechanisms to monitor infinite event streams, execute even in the absence of event inputs, enforce non-safety policies, and operate an enforcement model in which extraneous constraints such as transparency and uncontrollable events may be specified as meta-policies.
References
[1]
2018. Serverless Architecture Market Size, Share. Industry Report, 2018--2025. https://www.grandviewresearch.com/industry-analysis/serverless-architecture-market.
[2]
2018. Serverless. The Serverless Application Framework powered by AWS Lambda, API Gateway, and more. https://serverless.com/.
[3]
Luca Aceto, Antonis Achilleos, Adrian Francalanza, and Anna Ingólfsdóttir. 2018. Monitoring for silent actions. In 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik.
[4]
Bowen Alpern and Fred B Schneider. 1985. Defining liveness. Information processing letters 21, 4 (1985), 181--185.
[5]
Rajeev Alur and Pavol Černy. 2011. Streaming transducers for algorithmic verification of single-pass list-processing programs. In ACM SIGPLAN Notices, Vol. 46. ACM, 599--610.
[6]
Rajeev Alur, Loris DAntoni, Jyotirmoy Deshmukh, Mukund Raghothaman, and Yifei Yuan. 2013. Regular functions and cost register automata. In 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science. IEEE, 13--22.
[7]
Rajeev Alur, Dana Fisman, Konstantinos Mamouras, Mukund Raghothaman, and Caleb Stanford. 2018. Streamable regular transductions. arXiv preprint arXiv:1807.03865 (2018).
[8]
David Basin, Vincent Jugé, Felix Klaedtke, and Eugen Zălinescu. 2013. Enforceable security policies revisited. ACM Transactions on Information and System Security (TISSEC) 16, 1 (2013), 3.
[9]
Daniele Beauquier and J-E Pin. 1991. Languages and scanners. Theoretical Computer Science 84, 1 (1991), 3--21.
[10]
Nataliia Bielova and Fabio Massacci. 2011. Do you really mean what you actually enforced? International Journal of Information Security 10, 4 (2011), 239--254.
[11]
Michael R Clarkson and Fred B Schneider. 2010. Hyperproperties. Journal of Computer Security 18, 6 (2010), 1157--1210.
[12]
Volker Diekert, Anca Muscholl, and Igor Walukiewicz. 2015. A Note on Monitors and Büchi automata. In International Colloquium on Theoretical Aspects of Computing. Springer, 39--57.
[13]
Egor Dolzhenko, Jay Ligatti, and Srikar Reddy. 2015. Modeling runtime enforcement with mandatory results automata. International Journal of Information Security 14, 1 (2015), 47--60.
[14]
Manfred Droste, Werner Kuich, and Heiko Vogler. 2009. Handbook of weighted automata. Springer Science & Business Media.
[15]
Philip WL Fong. 2004. Access control by tracking shallow execution history. In Security and Privacy, 2004. Proceedings. 2004 IEEE Symposium on. IEEE, 43--55.
[16]
Paul German. 2016. Face the facts-your organisation will be breached. Network Security 2016, 8 (2016), 9--10.
[17]
Raphaël Khoury and Sylvain Hallé. 2015. Runtime enforcement with partial control. In International Symposium on Foundations and Practice of Security. Springer, 102--116.
[18]
Raphaël Khoury and Nadia Tawbi. 2015. Equivalence-preserving corrective enforcement of security properties. International Journal of Information and Computer Security 7, 2--4 (2015), 113--139.
[19]
Sathish Alampalayam Kumar, Tyler Vealey, and Harshit Srivastava. 2016. Security in internet of things: Challenges, solutions and future directions. In System Sciences (HICSS), 2016 49th Hawaii International Conference on. IEEE, 5772--5781.
[20]
Leslie Lamport. 1977. Proving the correctness of multiprocess programs. IEEE transactions on software engineering 2 (1977), 125--143.
[21]
Jay Ligatti, Lujo Bauer, and David Walker. 2005. Edit automata: Enforcement mechanisms for run-time security policies. International Journal of Information Security 4, 1--2 (2005), 2--16.
[22]
Jay Ligatti, Lujo Bauer, and David Walker. 2009. Run-time enforcement of nonsafety policies. ACM Transactions on Information and System Security (TISSEC) 12, 3 (2009), 19.
[23]
Nancy A Lynch and Mark R Tuttle. 1988. An introduction to input/output automata. Laboratory for Computer Science, Massachusetts Institute of Technology.
[24]
Yannis Mallios, Lujo Bauer, Dilsun Kaynar, and Jay Ligatti. 2012. Enforcing more with less: Formalizing target-aware run-time monitors. In International Workshop on Security and Trust Management. Springer, 17--32.
[25]
Patrick McDaniel and Stephen McLaughlin. 2009. Security and privacy challenges in the smart grid. IEEE Security & Privacy 7, 3 (2009).
[26]
George H Mealy. 1955. A method for synthesizing sequential circuits. The Bell System Technical Journal 34, 5 (1955), 1045--1079.
[27]
Shanmugavelayutham Muthukrishnan et al. 2005. Data streams: Algorithms and applications. Foundations and Trends® in Theoretical Computer Science 1, 2 (2005), 117--236.
[28]
Minh Ngo, Fabio Massacci, Dimiter Milushev, and Frank Piessens. 2015. Runtime enforcement of security policies on black box reactive programs. In ACM SIGPLAN Notices, Vol. 50. ACM, 43--54.
[29]
Srinivas Pinisetty, Viorel Preoteasa, Stavros Tripakis, Thierry Jéron, Yliès Falcone, and Hervé Marchand. 2017. Predictive runtime enforcement. Formal Methods in System Design 51, 1 (2017), 154--199.
[30]
Matthieu Renard, Yliès Falcone, Antoine Rollet, Srinivas Pinisetty, Thierry Jéron, and Hervé Marchand. 2015. Enforcement of (timed) properties with uncontrollable events. In International Colloquium on Theoretical Aspects of Computing. Springer, 542--560.
[31]
Fred B Schneider. 2000. Enforceable security policies. ACM Transactions on Information and System Security (TISSEC) 3, 1 (2000), 30--50.
[32]
Chamseddine Talhi, Nadia Tawbi, and Mourad Debbabi. 2008. Execution monitoring enforcement under memory-limitation constraints. Information and Computation 206, 2 (2008), 158--184.
[33]
Mahesh Viswanathan and Moonzoo Kim. 2004. Foundations for the run-time monitoring of reactive systems-fundamentals of the mac language. In International Colloquium on Theoretical Aspects of Computing. Springer, 543--556.
Recommendations
Modeling runtime enforcement with mandatory results automata
This paper presents a theory of runtime enforcement based on mechanism models called mandatory results automata (MRAs). MRAs can monitor and transform security-relevant actions and their results. The operational semantics of MRAs is simple and enables ...
Run-Time Enforcement of Nonsafety Policies
A common mechanism for ensuring that software behaves securely is to monitor programs at run time and check that they dynamically adhere to constraints specified by a security policy. Whenever a program monitor detects that untrusted software is ...
Edit automata: enforcement mechanisms for run-time security policies
We analyze the space of security policies that can be enforced by monitoring and modifying programs at run time. Our program monitors, called edit automata, are abstract machines that examine the sequence of application program actions and transform the ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
February 2020
382 pages
ISBN:9781450376655
DOI:10.1145/3384544
Copyright © 2020 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 17 April 2020
Check for updates
Author Tags
Qualifiers
- Research-article
- Research
- Refereed limited
Conference
ICSCA 2020
ICSCA 2020: 2020 9th International Conference on Software and Computer Applications
February 18 - 21, 2020
Langkawi, Malaysia
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 113Total Downloads
- Downloads (Last 12 months)5
- Downloads (Last 6 weeks)0
Reflects downloads up to 25 Jan 2025
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in