Sage Journals: Discover world-class research

Abstract

This paper presents a formal framework for run-time enforcement mechanisms, or monitors, based on probabilistic input/output automata [Task-structured probabilistic I/O automata, Technical Report MIT-CSAIL-TR-2006-060, 2006; Proceedings of the 8th International Workshop on Discrete Event Systems, 2006, pp. 207–214], which allows for the modeling of complex and interactive systems. We associate with each trace of a monitored system (i.e., a monitor interposed between a system and an environment) a probability and a real number that represents the cost that the actions appearing on the trace incur on the monitored system. This allows us to calculate the probabilistic (expected) cost of the monitor and the monitored system, which we use to classify monitors, not only in the typical sense, as sound and transparent [ACM Transactions on Information and System Security 12(3) (2009), 1–41], but also at a more fine-grained level, as cost-optimal or cost-efficient. We show how a cost-optimal monitor can be built using information about cost and the probabilistic future behavior of the system and the environment, showing how deeper knowledge of a system can lead to construction of more efficient security mechanisms.

Keywords

Security policies monitoring cost probabilistic I/O automata policy enforcement

Get full access to this article

View all access options for this article.

References

[1]

Appel, Modern Compiler Implementation in ML: Basic Techniques, Cambridge Univ. Press, 1997.

[2]

Baier,

Grober,

Leucker,

Bollig and

Ciesinski, Controller synthesis for probabilistic systems, in: Proceedings of IFIP TCS, 2004.

[3]

Barringer,

Goldberg,

Havelund and

Koushik, Program monitoring with LTL in EAGLE, in: Proceedings of the 18th International Parallel and Distributed Processing Symposium, 2004.

[4]

Basin,

Jugé,

Klaedtke and

Zălinescu, Enforceable security policies revisited, in: Proceedings of POST 2012, Lecture Notes in Computer Science, Vol. 7215, 2012, pp. 309–328.

[5]

Basin,

E.-R.

Olderog and

P.E.

Sevinc, Specifying and analyzing security automata using CSP-OZ, in: Proceedings ACM Symposium on Information, Computer and Communications Security (ASIACCS), 2007, pp. 70–81.

[6]

Bauer,

Leucker and

Schallhart, Runtime verification for LTL and TLTL, ACM Trans. Softw. Eng. Methodol. 20(4) (2011), 1–64.

[7]

Bielova and

Massacci, Predictability of enforcement, in: Proceedings of the International Symposium on Engineering Secure Software and Systems, 2011, pp. 73–86.

[8]

Blakley,

McDermott and

Geer, Information security is information risk management, in: Proceedings of the 2001 Workshop on New Security Paradigms, 2001, pp. 97–104.

[9]

Canetti,

Cheung,

Kaynar,

Liskov,

Lynch,

Pereira and

Segala, Task-structured probabilistic I/O automata, Technical Report MIT-CSAIL-TR-2006-060, 2006.

10.

[10]

Canetti,

Cheung,

Kaynar,

Liskov,

Lynch,

Pereira and

Segala, Task-structured probabilistic I/O automata, in: Proceedings of the 8th International Workshop on Discrete Event Systems, 2006, pp. 207–214.

11.

[11]

Caravagna,

Costa and

Pardini, Lazy security controllers, in: Proceedings of the 8th International Workshop on Security and Trust Management (STM 2012), 2013, pp. 33–48.

12.

[12]

Chatterjee,

Doyen and

T.A.

Henzinger, Quantitative languages, in: Proceedings of the 17th International Conference on Computer Science Logic (CSL), 2008, pp. 385–400.

13.

[13]

P.-C.

Cheng,

Rohatgi,

Keser,

P.A.

Karger,

G.M.

Wagner and

A.S.

Reninger, Fuzzy multi-level security: An experiment on quantified risk-adaptive access control, in: Proceedings of the 2007 IEEE Symposium on Security and Privacy, 2007, pp. 222–230.

14.

[14]

M.R.

Clarkson and

F.B.

Schneider, Hyperproperties, J. Comput. Secur. 18(6) (2010), 1157–1210.

15.

[15]

Drábik,

Martinelli and

Morisset, A quantitative approach for inexact enforcement of security policies, in: Proceedings of the 15th International Conference on Information Security, ISC’12, 2012, pp. 306–321.

16.

[16]

Drábik,

Martinelli and

Morisset, Cost-aware runtime enforcement of security policies, in: Proceedings of the 8th International Workshop on Security and Trust Management (STM 2012), 2013, pp. 1–16.

17.

[17]

Easwaran,

Kannan and

Lee, Optimal control of software ensuring safety and functionality, Technical Report MS-CIS-05-20, University of Pennsylvania, 2005.

18.

[18]

Erlingsson, The inlined reference monitor approach to security policy enforcement, PhD thesis, Ithaca, NY, USA, 2004.

19.

[19]

Falcone,

J.-C.

Fernandez and

Mounier, What can you verify and enforce at runtime?, International Journal on Software Tools for Technology Transfer (STTT) 14(3) (2012), 349–382.

20.

[20]

P.W.

Fong, Access control by tracking shallow execution history, in: Proceedings of the 2004 IEEE Symposium on Security and Privacy, 2004, pp. 43–55.

21.

[21]

Gay,

Mantel and

Sprick, Service automata, in: Proceedings of the 8th International Conference on Formal Aspects of Security and Trust, 2012, pp. 148–163.

22.

[22]

K.W.

Hamlen,

Morrisett and

F.B.

Schneider, Computability classes for enforcement mechanisms, ACM Trans. Program. Lang. Syst. 28(1) (2006), 175–205.

23.

[23]

Kwiatkowska, Survey of fairness notions, Information and Software Technology 31(7) (1989), 371–386.

24.

[24]

Ligatti,

Bauer and

Walker, Edit automata: Enforcement mechanisms for run-time security policies, International Journal of Information Security 4(1-2) (2005), 2–16.

25.

[25]

Ligatti,

Bauer and

Walker, Run-time enforcement of nonsafety policies, ACM Transactions on Information and System Security 12(3) (2009), 1–41.

26.

[26]

Ligatti and

Reddy, A theory of runtime enforcement, with results, in: Computer Security – ESORICS 2010, Lecture Notes in Computer Science, Vol. 6345, 2010, pp. 87–100.

27.

[27]

G.R.

Malan,

Watson,

Jahanian and

Howell, Transport and application protocol scrubbing, in: Proceedings of INFOCOM 2000, 2000, pp. 1381–1390.

28.

[28]

Mallios,

Bauer,

Kaynar and

Ligatti, Enforcing more with less: Formalizing target-aware run-time monitors, Technical Report CMU-CyLab-12-009, CyLab, Carnegie Mellon University, 2012.

29.

[29]

Mallios,

Bauer,

Kaynar and

Ligatti, Enforcing more with less: Formalizing target-aware run-time monitors, in: Proceedings of the 8th International Workshop on Security and Trust Management (STM 2012), 2013, pp. 17–32.

30.

[30]

Martinelli and

Matteucci, Through modeling to synthesis of security automata, Electron. Notes Theor. Comput. Sci. 179 (2007), 31–46.

31.

[31]

Martinelli,

Matteucci and

Morisset, From qualitative to quantitative enforcement of security policy, in: Proceedings of the 6th International Conference on Mathematical Methods, Models and Architectures for Computer Network Security: Computer Network Security, MMM-ACNS’12, 2012, pp. 22–35.

32.

[32]

Martinelli and

Morisset, Quantitative access control with partially-observable Markov decision processes, in: Proceedings of the Second ACM Conference on Data and Application Security and Privacy, CODASPY’12, 2012, pp. 169–180.

33.

[33]

Nain and

M.Y.

Vardi, Synthesizing probabilistic composers, in: Proceedings of the 15th International Conference on Foundations of Software Science and Computational Structures, 2012, pp. 421–436.

34.

[34]

Roşu and

Bensalem, Allen linear (interval) temporal logic – Translation to LTL and monitor synthesis, in: Proceedings of the 18th International Conference on Computer Aided Verification, 2006, pp. 263–277.

35.

[35]

Roşu,

Chen and

Ball, Synthesizing monitors for safety properties: This time with calls and returns, in: Proceedings of Runtime Verification, 2008, pp. 51–68.

36.

[36]

F.B.

Schneider, Enforceable security policies, ACM Trans. Inf. Syst. Secur. 3 (2000), 30–50.

37.

[37]

Xie,

Mead,

Chen,

Dean,

Lopez,

Ojoko-Adams and

Osman, SQUARE project: Cost/benefit analysis framework for information security improvement projects in small companies, Technical Report CMU/SEI-2004-TN-045, Software Engineering Institute, Carnegie Mellon University, 2004.

Probabilistic cost enforcement of security policies

Abstract

Keywords

Get full access to this article

References