Journal Title
Title of Journal: Form Asp Comp
|
Abbravation: Formal Aspects of Computing
|
Publisher
Springer-Verlag
|
|
|
|
Authors: Thai Son Hoang
Publish Date: 2012/06/29
Volume: 25, Issue: 1, Pages: 59-87
Abstract
The Shadow semantics is a qualitative model for noninterference security for sequential programs In this paper we first extend the Shadow semantics to EventB to reason about discrete transition systems with noninterference security properties In particular we investigate how these security properties can be specified and proved as machine invariants Next we highlight the role of security invariants during refinement and identify some common patterns in specifying them Finally we propose a practical extension to the supporting Rodin platform of EventB with the possibility of having some properties to be invariantsbyconstruction
Keywords:
.
|
Other Papers In This Journal:
|