CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Idea: Unwinding Based Model-Checking and Testing for Non-Interference on EFSMs

M. Ochoa ; J. Cuellar ; A. Pretschner ; Per A. Hallgren (Institutionen för data- och informationsteknik, Nätverk och system, Datakommunikation och distribuerade system (Chalmers))
Engineering Secure Software and Systems (0302-9743). Vol. 8978 (2015), p. 34-42.
[Konferensbidrag, refereegranskat]

Undesired flows of information between different sensitivity levels or domains can seriously compromise the security of a system. Moreover, even if specifications are secure, unwanted flows can still be present in implementations. In this paper we present a model-based technique to discover unwanted information flows in specifications and to test systems for unwanted flows. We base our approach on an unwinding relation for Extended Finite State Machines. We preliminary validate our approach by means of an implementation that allows us to benchmark the efficiency of our model-checking algorithm.

Denna post skapades 2015-10-21.
CPL Pubid: 224569