Wyniki wyszukiwania - BazTech

Ograniczanie wyników

2 Fundamenta Informaticae

Znaleziono wyników: 2

Liczba wyników na stronie

Wyniki wyszukiwania

Sortuj według:

Ogranicz wyniki do:

Abstract Interpretation and Model Checking for Checking Secure Information Flow in Concurrent Systems

De Francesco N., Santone A., Tesei L.

Fundamenta Informaticae

2003

Vol. 54, nr 2,3

195-211

We propose a method to check secure information flow in concurrent programs with synchronization. The method is based on the combination of abstract interpretation and model checking: by abstract interpretation we build a finite representation (transition system) of the behavior of the program. Then we model check the the abstract transition system with respect to the security properties, expressed by a set of temporal logic formulae. The approach allows certifying more programs than previous methods do. The main point is that we are able to check more carefully the scope of indirect information flows.

A Notion of Non-Interference for Timed Automata

Barbuti R., De Francesco N., Santone A., Tesei L.

Fundamenta Informaticae

2002

Vol. 51, nr 1,2

1-11

The non-interference property of concurrent systems is a security property concerning the flow of information among different levels of security of the system. In this paper we introduce a notion of timed non-interference for real-time systems specified by timed automata. The notion is presented using an automata based approach and then it is characterized also by operations and equivalence between timed languages. The definition is applied to an example of a time-critical system modeling a simplified control of an airplane.