Showing 1–5 of 5 results for author: Clarkson, M R

Checking Interaction-Based Declassification Policies for Android Using Symbolic Execution

Authors: Kristopher Micinski, Jonathan Fetter-Degges, **seong Jeon, Jeffrey S. Foster, Michael R. Clarkson

Abstract: Mobile apps can access a wide variety of secure information, such as contacts and location. However, current mobile platforms include only coarse access control mechanisms to protect such data. In this paper, we introduce interaction-based declassification policies, in which the user's interactions with the app constrain the release of sensitive information. Our policies are defined extensionally,… ▽ More Mobile apps can access a wide variety of secure information, such as contacts and location. However, current mobile platforms include only coarse access control mechanisms to protect such data. In this paper, we introduce interaction-based declassification policies, in which the user's interactions with the app constrain the release of sensitive information. Our policies are defined extensionally, so as to be independent of the app's implementation, based on sequences of security-relevant events that occur in app runs. Policies use LTL formulae to precisely specify which secret inputs, read at which times, may be released. We formalize a semantic security condition, interaction-based noninterference, to define our policies precisely. Finally, we describe a prototype tool that uses symbolic execution to check interaction-based declassification policies for Android, and we show that it enforces policies correctly on a set of apps. △ Less

Submitted 29 July, 2015; v1 submitted 14 April, 2015; originally announced April 2015.

Comments: This research was supported in part by NSF grants CNS-1064997 and 1421373, AFOSR grants FA9550-12-1-0334 and FA9550-14-1-0334, a partnership between UMIACS and the Laboratory for Telecommunication Sciences, and the National Security Agency

Temporal Logics for Hyperproperties

Authors: Michael R. Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K. Micinski, Markus N. Rabe, César Sánchez

Abstract: Two new logics for verification of hyperproperties are proposed. Hyperproperties characterize security policies, such as noninterference, as a property of sets of computation paths. Standard temporal logics such as LTL, CTL, and CTL* can refer only to a single path at a time, hence cannot express many hyperproperties of interest. The logics proposed here, HyperLTL and HyperCTL*, add explicit and s… ▽ More Two new logics for verification of hyperproperties are proposed. Hyperproperties characterize security policies, such as noninterference, as a property of sets of computation paths. Standard temporal logics such as LTL, CTL, and CTL* can refer only to a single path at a time, hence cannot express many hyperproperties of interest. The logics proposed here, HyperLTL and HyperCTL*, add explicit and simultaneous quantification over multiple paths to LTL and to CTL*. This kind of quantification enables expression of hyperproperties. A model checking algorithm for the proposed logics is given. For a fragment of HyperLTL, a prototype model checker has been implemented. △ Less

Submitted 20 January, 2014; v1 submitted 17 January, 2014; originally announced January 2014.

A Temporal Logic of Security

Authors: Masoud Koleini, Michael R. Clarkson, Kristopher K. Micinski

Abstract: A new logic for verification of security policies is proposed. The logic, HyperLTL, extends linear-time temporal logic (LTL) with connectives for explicit and simultaneous quantification over multiple execution paths, thereby enabling HyperLTL to express information-flow security policies that LTL cannot. A model-checking algorithm for a fragment of HyperLTL is given, and the algorithm is implemen… ▽ More A new logic for verification of security policies is proposed. The logic, HyperLTL, extends linear-time temporal logic (LTL) with connectives for explicit and simultaneous quantification over multiple execution paths, thereby enabling HyperLTL to express information-flow security policies that LTL cannot. A model-checking algorithm for a fragment of HyperLTL is given, and the algorithm is implemented in a prototype model checker. The class of security policies expressible in HyperLTL is characterized by an arithmetic hierarchy of hyperproperties. △ Less

Submitted 9 July, 2013; v1 submitted 24 June, 2013; originally announced June 2013.

Belief Semantics of Authorization Logic

Authors: Andrew K. Hirsch, Michael R. Clarkson

Abstract: Authorization logics have been used in the theory of computer security to reason about access control decisions. In this work, a formal belief semantics for authorization logics is given. The belief semantics is proved to subsume a standard Kripke semantics. The belief semantics yields a direct representation of principals' beliefs, without resorting to the technical machinery used in Kripke seman… ▽ More Authorization logics have been used in the theory of computer security to reason about access control decisions. In this work, a formal belief semantics for authorization logics is given. The belief semantics is proved to subsume a standard Kripke semantics. The belief semantics yields a direct representation of principals' beliefs, without resorting to the technical machinery used in Kripke semantics. A proof system is given for the logic; that system is proved sound with respect to the belief and Kripke semantics. The soundness proof for the belief semantics, and for a variant of the Kripke semantics, is mechanized in Coq. △ Less

Submitted 3 August, 2013; v1 submitted 8 February, 2013; originally announced February 2013.

Nexus Authorization Logic (NAL): Logical Results

Authors: Andrew K. Hirsch, Michael R. Clarkson

Abstract: Nexus Authorization Logic (NAL) [Schneider et al. 2011] is a logic for reasoning about authorization in distributed systems. A revised version of NAL is given here, including revised syntax, a revised proof theory using localized hypotheses, and a new Kripke semantics. The proof theory is proved sound with respect to the semantics, and that proof is formalized in Coq. Nexus Authorization Logic (NAL) [Schneider et al. 2011] is a logic for reasoning about authorization in distributed systems. A revised version of NAL is given here, including revised syntax, a revised proof theory using localized hypotheses, and a new Kripke semantics. The proof theory is proved sound with respect to the semantics, and that proof is formalized in Coq. △ Less

Submitted 15 November, 2012; v1 submitted 15 November, 2012; originally announced November 2012.