Iterative Analysis to Improve Key Properties of Critical Human-Intensive Processes: An Election Security Example

Citation

L. Osterweil, M. Bishop, H. Conboy, H. Phan, B. Simidchieva, G. Avrunin, L. Clarke, and S. Peisert, “Iterative Analysis to Improve Key Properties of Critical Human-Intensive Processes: An Election Security Example,” ACM Transactions on Privacy and Security 20(2) pp. 5:1–5:30 (Mar. 2017).

Paper

• Published version web page, free at ACM Digital Library []
• Published version web page, paper paywalled at ACM Digital Library: [DOI] [URL]
• Authors’ final version:
  • Local: [PDF] [PS]
  • UC Repository: [eScholarship]

Abstract

In this article, we present an approach for systematically improving complex processes, especially those involving human agents, hardware devices, and software systems. We illustrate the utility of this approach by applying it to part of an election process and show how it can improve the security and correctness of that subprocess. We use the Little-JIL process definition language to create a precise and detailed definition of the process. Given this process definition, we use two forms of automated analysis to explore whether specified key properties, such as security and safety policies, can be undermined. First, we use model checking to identify process execution sequences that fail to conform to event-sequence properties. After these are addressed, we apply fault tree analysis to identify when the misperformance of steps might allow undesirable outcomes, such as security breaches. The results of these analyses can provide assurance about the process; suggest areas for improvement; and, when applied to a modified process definition, evaluate proposed changes.

Bibliographic Information: [BibTeX] [EndNote] [RIS]
DOI: 10.1145/3041041