CAMPUS è l'Archivio istituzionale delle pubblicazioni scientifiche dell’Università di Camerino. E’ un sistema aperto, pubblico e interoperabile che raccoglie, conserva ed espone i dati relativi alle attività e ai prodotti della ricerca dell’Ateneo con lo scopo di migliorarne la visibilità e di favorirne l’impatto a livello nazionale e internazionale.
EnglishWe 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 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.
Scheda prodotto non validato
Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo
| Titolo: | Abstract Interpretation and Model Checking for Checking Secure Information Flow in Concurrent Systems |
| Autori: | |
| Data di pubblicazione: | 2003 |
| Rivista: | |
| Handle: | http://hdl.handle.net/11581/201302 |
| Appare nelle tipologie: | Articolo |
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Utilizza questo identificativo per citare o creare un link a questo documento:
http://hdl.handle.net/11581/201302
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
Copyright © 2021