Entry Jayaraman:2013:MAR 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{Jayaraman:2013:MAR,
  author =       "Karthick Jayaraman and Mahesh Tripunitara and Vijay
                 Ganesh and Martin Rinard and Steve Chapin",
  title =        "{Mohawk}: Abstraction-Refinement and Bound-Estimation
                 for Verifying Access Control Policies",
  journal =      j-TISSEC,
  volume =       "15",
  number =       "4",
  pages =        "18:1--18:??",
  month =        apr,
  year =         "2013",
  CODEN =        "ATISBQ",
  DOI =          "https://doi.org/10.1145/2445566.2445570",
  ISSN =         "1094-9224 (print), 1557-7406 (electronic)",
  ISSN-L =       "1094-9224",
  bibdate =      "Thu Apr 4 18:18:20 MDT 2013",
  bibsource =    "http://portal.acm.org/;
                 http://www.math.utah.edu/pub/tex/bib/tissec.bib",
  abstract =     "Verifying that access-control systems maintain desired
                 security properties is recognized as an important
                 problem in security. Enterprise access-control systems
                 have grown to protect tens of thousands of resources,
                 and there is a need for verification to scale
                 commensurately. We present techniques for
                 abstraction-refinement and bound-estimation for bounded
                 model checkers to automatically find errors in
                 Administrative Role-Based Access Control (ARBAC)
                 security policies. ARBAC is the first and most
                 comprehensive administrative scheme for Role-Based
                 Access Control (RBAC) systems. In the
                 abstraction-refinement portion of our approach, we
                 identify and discard roles that are unlikely to be
                 relevant to the verification question (the abstraction
                 step). We then restore such abstracted roles
                 incrementally (the refinement steps). In the
                 bound-estimation portion of our approach, we lower the
                 estimate of the diameter of the reachability graph from
                 the worst-case by recognizing relationships between
                 roles and state-change rules. Our techniques complement
                 one another, and are used with conventional bounded
                 model checking. Our approach is sound and complete: an
                 error is found if and only if it exists. We have
                 implemented our technique in an access-control policy
                 analysis tool called Mohawk. We show empirically that
                 Mohawk scales well to realistic policies, and provide a
                 comparison with prior tools.",
  acknowledgement = ack-nhfb,
  articleno =    "18",
  fjournal =     "ACM Transactions on Information and System Security",
  journal-URL =  "http://portal.acm.org/browse_dl.cfm?idx=J789",
}

Related entries