More and more software libraries and applications in high-performance computing and distributed systems are coded using the Java programming language. The correctness of such pieces of code w.r.t. a given set of security policies often depends on the correct handling of timing between concurrent or recurrent events. Model-checking has proven to be an effective tool for verifying the correctness of software. In spite of the growing importance of this application area of formal methods, though, no approach exists that targets the problem of verifying the correctness of real-Time software w.r.t.Timed specifications. The few existing works focus on very different problems, such as schedulability analysis of Java tasks. In this paper we present an approach combining rule-based static analysis together with symbolic execution of Java code to extract networks of timed automata from existing software and then use Uppaal to model-check them against timed specifications. We show through a real-world case study that this approach can be helpful in model-checking security policies of real-Time Java software.

Towards model checking security of real time Java software

Spalazzi, Luca;Spegni, Francesco;
2018

Abstract

More and more software libraries and applications in high-performance computing and distributed systems are coded using the Java programming language. The correctness of such pieces of code w.r.t. a given set of security policies often depends on the correct handling of timing between concurrent or recurrent events. Model-checking has proven to be an effective tool for verifying the correctness of software. In spite of the growing importance of this application area of formal methods, though, no approach exists that targets the problem of verifying the correctness of real-Time software w.r.t.Timed specifications. The few existing works focus on very different problems, such as schedulability analysis of Java tasks. In this paper we present an approach combining rule-based static analysis together with symbolic execution of Java code to extract networks of timed automata from existing software and then use Uppaal to model-check them against timed specifications. We show through a real-world case study that this approach can be helpful in model-checking security policies of real-Time Java software.
9781538678787
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: http://hdl.handle.net/11566/265853
 Attenzione

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

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