Formal Mental Models for Human-Centered Cybersecurity

Abstract

Human users are increasingly recognized as a vector of cybersecurity attack. One problem that contributes to this condition is the growing complexity of digital tools. Such complexity can make it difficult for users to understand how tools work and how their actions will impact security. This work sought to answer the research question: Can mental modeling analyses (from human factors engineering and human-automation interaction) be developed to effectively discover cybersecurity risks? To answer this, we extend mental models with cybersecurity-specific concepts. The resulting models are then incorporated into model checking analyses (an automated approach to formal verification) to discover if and when mismatches between human mental models and systems can cause security failures. We evaluated our approach by successfully applying it to a case study regarding the security configuration of a popular cloud data storage service. We ultimately discuss the results of this analysis and outline future research possibilities.

Keywords:

• Cybersecurity
• mental
• models
• model
• checking
• formal
• methods
• mode confusion
• human error

Disclosure statement

No potential conflict of interest was reported by the author(s).

Notes

1 All the information presented in this article was true as of April 2018. Publication was deferred to offer sufficient time to address issues disclosed herein. The actual name of the cloud computing system evaluated has also been removed to mitigate risks of exposing the system and its users to attack; A full listing of the created model can be found at https://tinyurl.com/2p8aeaev.

2 It is our understanding that improved user alerting when creating certain unprotected, publicly-accessible resources is one of several changes implemented since this research was performed.

3 http://sal.csl.sri.com/index.shtml.

4 A full listing of counterexamples found for all reported analyses are available at https://tinyurl.com/2p8aeaev.

Additional information

Notes on contributors

Adam M. Houser

Adam M. Houser received the Ph.D. in industrial engineering from the State University of New York at Buffalo in Buffalo, New York, USA in 2018. Since then, he has worked at the Johns Hopkins University Applied Physics Laboratory as a senior systems engineer.

Matthew L. Bolton

Matthew Bolton is an Associate Professor of Systems and Information Engineering at the University of Virginia. He obtained his Ph.D. in Systems Engineering from UVA in 2010. He previously held academic appointments at the University of Illinois in Chicago and the University at Buffalo.