We present an approach enabling end-users to prove security properties of the Java bytecode by statically analysing the code itself, thus eliminating the run time check for the access permission. The approach is based on the combination of two well-known techniques: abstract interpretation and model checking. By means of an operational abstract semantics of the bytecode, we built a finite transition system embodying security informations and abstracting from actual values. Then we model check it against some formulae expressing security properties. We use the SMV model checker. A main point of the paper is the definition of the properties that the abstract semantics must satisfy to ensure the absence of security leakages.

Combining Abstract Interpretation and Model Checking for Analysing Security Properties of Java Bytecode

BERNARDESCHI, CINZIA;DE FRANCESCO, NICOLETTA
2002-01-01

Abstract

We present an approach enabling end-users to prove security properties of the Java bytecode by statically analysing the code itself, thus eliminating the run time check for the access permission. The approach is based on the combination of two well-known techniques: abstract interpretation and model checking. By means of an operational abstract semantics of the bytecode, we built a finite transition system embodying security informations and abstracting from actual values. Then we model check it against some formulae expressing security properties. We use the SMV model checker. A main point of the paper is the definition of the properties that the abstract semantics must satisfy to ensure the absence of security leakages.
2002
9783540436317
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/205464
 Attenzione

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

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