research-article

Predictive runtime enforcement

Authors:

Hervé MarchandAuthors Info & Claims

SAC '16: Proceedings of the 31st Annual ACM Symposium on Applied Computing

Pages 1628 - 1633

https://doi.org/10.1145/2851613.2851827

Published: 04 April 2016 Publication History

Get Access

Abstract

Runtime enforcement (RE) is a technique to ensure that the (untrustworthy) output of a black-box system satisfies some desired properties. In RE, the output of the running system, modeled as a stream of events, is fed into an enforcement monitor. The monitor ensures that the stream complies with a certain property, by delaying or modifying events if necessary. This paper deals with predictive runtime enforcement, where the system is not entirely black-box, but we know something about its behavior. This a-priori knowledge about the system allows to output some events immediately, instead of delaying them until more events are observed, or even blocking them permanently. This in turn results in better enforcement policies. We also show that if we have no knowledge about the system, then the proposed enforcement mechanism reduces to a classical non-predictive RE framework. All our results are formalized and proved in the Isabelle theorem prover.

References

[1]

R. Bloem, B. Könighofer, R. Könighofer, and C. Wang. Shield synthesis: Runtime enforcement for reactive systems. In TACAS, volume 9035 of LNCS. Springer, 2015.

Digital Library

Google Scholar

[2]

C. G. Cassandras and S. Lafortune. Introduction to Discrete Event Systems. Springer-Verlag New York, Inc., Secaucus, NJ, USA, 2006.

Digital Library

Google Scholar

[3]

H. Chabot, R. Khoury, and N. Tawbi. Extending the enforcement power of truncation monitors using static analysis. Computers & Security, 30(4):194--207, 2011.

Digital Library

Google Scholar

[4]

E. Dolzhenko, J. Ligatti, and S. Reddy. Modeling runtime enforcement with mandatory results automata. Int. J. Inf. Sec., 14(1):47--60, 2015.

Digital Library

Google Scholar

[5]

Y. Falcone, J.-C. Fernandez, and L. Mounier. Synthesizing enforcement monitors wrt. the safety-progress classification of properties. In Information Systems Security, volume 5352 of LNCS, pages 41--55. Springer Berlin Heidelberg, 2008.

Digital Library

Google Scholar

[6]

Y. Falcone, L. Mounier, J.-C. Fernandez, and J.-L. Richier. Runtime enforcement monitors: composition, synthesis, and enforcement abilities. Formal Methods in System Design, 38(3):223--262, 2011.

Digital Library

Google Scholar

[7]

J. Ligatti, L. Bauer, and D. Walker. Run-time enforcement of nonsafety policies. ACM Trans. Inf. Syst. Secur., 12(3):19:1--19:41, Jan. 2009.

Digital Library

Google Scholar

[8]

G. R. Malan, D. Watson, F. Jahanian, and P. Howell. Transport and application protocol scrubbing. In Proceedings IEEE INFOCOM 2000, Israel, pages 1381--1390, 2000.

Crossref

Google Scholar

[9]

T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL --- A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002.

Digital Library

Google Scholar

[10]

S. Pinisetty, Y. Falcone, T. Jéron, H. Marchand, A. Rollet, and O. Nguena Timo. Runtime enforcement of timed properties revisited. Formal Methods in System Design, 45(3):381--422, 2014.

Digital Library

Google Scholar

[11]

G. Rosu. On safety properties and their monitoring. Sci. Ann. Comp. Sci., 22(2):327--365, 2012.

Google Scholar

[12]

F. B. Schneider. Enforceable security policies. ACM Trans. Inf. Syst. Secur., 3(1):30--50, Feb. 2000.

Digital Library

Google Scholar

[13]

X. Zhang, M. Leucker, and W. Dong. Runtime verification with predictive semantics. In NASA Formal Methods - 4th International Symposium, volume 7226 of LNCS, pages 418--432. Springer, 2012.

Digital Library

Google Scholar

Cited By

View all

Sheikhi SMehmood UBak SSmolka SStoller S(2024)The black-box simplex architecture for runtime assurance of multi-agent CPSInnovations in Systems and Software Engineering10.1007/s11334-024-00553-6Online publication date: 21-Mar-2024
https://doi.org/10.1007/s11334-024-00553-6
Wenzel JKöhl MSterz SZhang HSchmidt AFetzer CHermanns H(2024)Traceability and Accountability by ConstructionLeveraging Applications of Formal Methods, Verification and Validation. Software Engineering Methodologies10.1007/978-3-031-75387-9_16(258-280)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1007/978-3-031-75387-9_16
Pinisetty SPradhan ARoop PTripakis S(2022)Compositional runtime enforcement revisitedFormal Methods in System Design10.1007/s10703-022-00401-y59:1-3(205-252)Online publication date: 26-Oct-2022
https://dl.acm.org/doi/10.1007/s10703-022-00401-y
Show More Cited By

Index Terms

Predictive runtime enforcement

Recommendations

Runtime Enforcement of Security Policies on Black Box Reactive Programs
POPL '15: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

Security enforcement mechanisms like execution monitors are used to make sure that some untrusted program complies with a policy. Different enforcement mechanisms have different strengths and weaknesses and hence it is important to understand the ...
Predictive runtime enforcement

Runtime enforcement (RE) is a technique to ensure that the (untrustworthy) output of a black-box system satisfies some desired properties. In RE, the output of the running system, modeled as a sequence of events, is fed into an enforcer. The enforcer ...
Runtime enforcement monitors: composition, synthesis, and enforcement abilities

Runtime enforcement is a powerful technique to ensure that a program will respect a given set of properties. We extend previous work on this topic in several directions. Firstly, we propose a generic notion of enforcement monitors based on a memory ...

Comments

Information & Contributors

Information

Published In

SAC '16: Proceedings of the 31st Annual ACM Symposium on Applied Computing

April 2016

2360 pages

ISBN:9781450337397

DOI:10.1145/2851613

Conference Chair:
Sascha Ossowski
University Rey Juan Carlos, Spain

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 the author(s) 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: 04 April 2016

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

SAC 2016

Sponsor:

SIGAPP

SAC 2016: Symposium on Applied Computing

April 4 - 8, 2016

Pisa, Italy

Acceptance Rates

SAC '16 Paper Acceptance Rate 252 of 1,047 submissions, 24%;

Overall Acceptance Rate 1,650 of 6,669 submissions, 25%

Upcoming Conference

SAC '25

Sponsor:
sigapp

The 40th ACM/SIGAPP Symposium on Applied Computing

March 31 - April 4, 2025

Catania , Italy

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

9
Total Citations
View Citations
110
Total Downloads

Downloads (Last 12 months)7
Downloads (Last 6 weeks)0

Reflects downloads up to 01 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Sheikhi SMehmood UBak SSmolka SStoller S(2024)The black-box simplex architecture for runtime assurance of multi-agent CPSInnovations in Systems and Software Engineering10.1007/s11334-024-00553-6Online publication date: 21-Mar-2024
https://doi.org/10.1007/s11334-024-00553-6
Wenzel JKöhl MSterz SZhang HSchmidt AFetzer CHermanns H(2024)Traceability and Accountability by ConstructionLeveraging Applications of Formal Methods, Verification and Validation. Software Engineering Methodologies10.1007/978-3-031-75387-9_16(258-280)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1007/978-3-031-75387-9_16
Pinisetty SPradhan ARoop PTripakis S(2022)Compositional runtime enforcement revisitedFormal Methods in System Design10.1007/s10703-022-00401-y59:1-3(205-252)Online publication date: 26-Oct-2022
https://dl.acm.org/doi/10.1007/s10703-022-00401-y
Colombo CPace GSchneider G(2021)Runtime Verification: Passing on the BatonFormal Methods in Outer Space10.1007/978-3-030-87348-6_5(89-107)Online publication date: 17-Oct-2021
https://doi.org/10.1007/978-3-030-87348-6_5
Falcone YMariani LRollet ASaha S(2018)Runtime Failure Prevention and ReactionLectures on Runtime Verification10.1007/978-3-319-75632-5_4(103-134)Online publication date: 11-Feb-2018
https://doi.org/10.1007/978-3-319-75632-5_4
Pinisetty SJron TTripakis SFalcone YMarchand HPreoteasa V(2017)Predictive runtime verification of timed propertiesJournal of Systems and Software10.1016/j.jss.2017.06.060132:C(353-365)Online publication date: 1-Oct-2017
https://dl.acm.org/doi/10.1016/j.jss.2017.06.060
Pinisetty SPreoteasa VTripakis SJéron TFalcone YMarchand H(2017)Predictive runtime enforcementFormal Methods in System Design10.1007/s10703-017-0271-151:1(154-199)Online publication date: 1-Aug-2017
https://dl.acm.org/doi/10.1007/s10703-017-0271-1
Bou-Ammar HJaber MNassar M(2017)Correctness-by-Learning of Infinite-State Component-Based SystemsFormal Aspects of Component Software10.1007/978-3-319-68034-7_10(162-178)Online publication date: 14-Sep-2017
https://doi.org/10.1007/978-3-319-68034-7_10
Pinisetty STripakis S(2016)Compositional Runtime EnforcementProceedings of the 8th International Symposium on NASA Formal Methods - Volume 969010.1007/978-3-319-40648-0_7(82-99)Online publication date: 7-Jun-2016
https://dl.acm.org/doi/10.1007/978-3-319-40648-0_7

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Abstract

References

Cited By

Index Terms

Recommendations

Runtime Enforcement of Security Policies on Black Box Reactive Programs