Formal Analysis and Verification of Systems Security Models with Gnosis

by Brian Monahan, Nick Papanikolaou
Abstract:
Emergent context-dependent non-functional re- quirements, such as those involving systems security activities and processes are, almost by definition, difficult to assess for their adequacy. One cannot easily anticipate and measure the effectiveness of systems defences in advance of actual field deployment until it is, of course, too late and the damage has been done. Our approach to security requirements assessment involves explicitly building systems security models using Gnosis, a process modelling simulation language developed at HP Labs. Gnosis models capture security situations which typically include aspects of the threat environment. In this paper we present the core aspects of this approach and discuss our latest work on developing explicit-state model checking of properties of multiple simulation runs.
Reference:
Formal Analysis and Verification of Systems Security Models with Gnosis (Brian Monahan, Nick Papanikolaou), 2012.
Bibtex Entry:
@MISC{Monahan2012a,
  author = {Brian Monahan and Nick Papanikolaou},
  title = {Formal Analysis and Verification of Systems Security Models with
	{G}nosis},
  month = may,
  year = {2012},
  abstract = {Emergent context-dependent non-functional re- quirements, such as
	those involving systems security activities and processes are, almost
	by definition, difficult to assess for their adequacy. One cannot
	easily anticipate and measure the effectiveness of systems defences
	in advance of actual field deployment until it is, of course, too
	late and the damage has been done. Our approach to security requirements
	assessment involves explicitly building systems security models using
	Gnosis, a process modelling simulation language developed at HP Labs.
	Gnosis models capture security situations which typically include
	aspects of the threat environment. In this paper we present the core
	aspects of this approach and discuss our latest work on developing
	explicit-state model checking of properties of multiple simulation
	runs.},
  owner = {papaniko},
  timestamp = {2012.05.24},
  url = {../files/monpap2.pdf}
}