We present a tool supporting the verification of programs written in stack-based assembly language against the secure information flow property. First, the tool builds the transition system, which corresponds to an abstract execution of the program, embodying security information and abstracting from the actual values. Then the states of the abstract transition system are checked to detect the satisfaction of the secure information flow property. The tool offers a windows user interface, through which the user can control the verification process, and observe the intermediate and final results.

An Abstract Semantics Tool for Secure Information Flow of Stack-based Assembly Programs

BERNARDESCHI, CINZIA;DE FRANCESCO, NICOLETTA;LETTIERI, GIUSEPPE
2002

Abstract

We present a tool supporting the verification of programs written in stack-based assembly language against the secure information flow property. First, the tool builds the transition system, which corresponds to an abstract execution of the program, embodying security information and abstracting from the actual values. Then the states of the abstract transition system are checked to detect the satisfaction of the secure information flow property. The tool offers a windows user interface, through which the user can control the verification process, and observe the intermediate and final results.
Bernardeschi, Cinzia; DE FRANCESCO, Nicoletta; Lettieri, Giuseppe
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11568/178386
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 12
  • ???jsp.display-item.citation.isi??? 8
social impact