Real-Time Policy Enforcement with Metric First-Order Temporal Logic


Date

2022

Publication Type

Conference Paper

ETH Bibliography

yes

Citations

Altmetric

Data

Abstract

Correctness and regulatory compliance of today’s software systems are crucial for our safety and security. This can be achieved with policy enforcement: the process of monitoring and possibly modifying system behavior to satisfy a given policy. The enforcer’s capabilities determine which policies are enforceable. We study the enforceability of policies specified in metric first-order temporal logic (MFOTL) with enforcers that can cause and suppress different system actions in real time. We consider an expressive safety fragment of MFOTL and show that a policy from that fragment is enforceable if and only if it is equivalent to a policy in a simpler, syntactically defined MFOTL fragment. We then propose an enforcement algorithm for all monitorable policies from the latter fragment, and show that our EnfPoly enforcer outperforms state-of-the-art tools.

Publication status

published

Book title

Computer Security – ESORICS 2022

Volume

13555

Pages / Article No.

211 - 232

Publisher

Springer

Event

27th European Symposium on Research in Computer Security (ESORICS 2022)

Edition / version

Methods

Software

Geographic location

Date collected

Date created

Subject

Organisational unit

03634 - Basin, David / Basin, David check_circle

Notes

Funding

Related publications and datasets