Entry Arkoudas:2014:SAC from tissec.bib

Last update: Sun Oct 15 02:58:48 MDT 2017                Valid HTML 3.2!

Index sections

Top | Symbols | Numbers | Math | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z

BibTeX entry

@Article{Arkoudas:2014:SAC,
  author =       "Konstantine Arkoudas and Ritu Chadha and Jason
                 Chiang",
  title =        "Sophisticated Access Control via {SMT} and Logical
                 Frameworks",
  journal =      j-TISSEC,
  volume =       "16",
  number =       "4",
  pages =        "17:1--17:??",
  month =        apr,
  year =         "2014",
  CODEN =        "ATISBQ",
  DOI =          "https://doi.org/10.1145/2595222",
  ISSN =         "1094-9224 (print), 1557-7406 (electronic)",
  ISSN-L =       "1094-9224",
  bibdate =      "Mon May 5 18:00:10 MDT 2014",
  bibsource =    "http://portal.acm.org/;
                 http://www.math.utah.edu/pub/tex/bib/tissec.bib",
  abstract =     "We introduce a new methodology for formulating,
                 analyzing, and applying access-control policies.
                 Policies are expressed as formal theories in the SMT
                 (satisfiability-modulo-theories) subset of typed
                 first-order logic, and represented in a programmable
                 logical framework, with each theory extending a core
                 ontology of access control. We reduce both request
                 evaluation and policy analysis to SMT solving, and
                 provide experimental results demonstrating the
                 practicality of these reductions. We also introduce a
                 class of canonical requests and prove that such
                 requests can be evaluated in linear time. In many
                 application domains, access requests are either
                 naturally canonical or can easily be put into canonical
                 form. The resulting policy framework is more expressive
                 than XACML and languages in the Datalog family, without
                 compromising efficiency. Using the computational logic
                 facilities of the framework, a wide range of
                 sophisticated policy analyses (including consistency,
                 coverage, observational equivalence, and change impact)
                 receive succinct formulations whose correctness can be
                 straightforwardly verified. The use of SMT solving
                 allows us to efficiently analyze policies with
                 complicated numeric (integer and real) constraints, a
                 weak point of previous policy analysis systems.
                 Further, by leveraging the programmability of the
                 underlying logical framework, our system provides
                 exceptionally flexible ways of resolving conflicts and
                 composing policies. Specifically, we show that our
                 system subsumes FIA (Fine-grained Integration Algebra),
                 an algebra recently developed for the purpose of
                 integrating complex policies.",
  acknowledgement = ack-nhfb,
  articleno =    "17",
  fjournal =     "ACM Transactions on Information and System Security",
  journal-URL =  "http://portal.acm.org/browse_dl.cfm?idx=J789",
}

Related entries