Automated Formal Verification of Application-specific Security Properties

Il contenuto (Full text) non è disponibile all'interno di questo archivio. Spedisci una richiesta all'autore per una copia del documento
Tipo di pubblicazione: Articolo in atti di convegno
Tipologia MIUR: Contributo in Atti di Convegno (Proceeding) > Contributo in atti di convegno
Titolo: Automated Formal Verification of Application-specific Security Properties
Autori: Bettassa Copet P.; Sisto R.
Autori di ateneo:
Intervallo pagine: pp. 45-59
Titolo del periodico: LECTURE NOTES IN COMPUTER SCIENCE
Tipo di referee: Comitato scientifico
Editore: Springer
ISBN: 9783319048963
ISSN: 0302-9743
Volume: 8364
Titolo del convegno: Engineering Secure Software and Systems (ESSOS)
Luogo dell'evento: Munich, Germany
Data dell'evento: 26-28/2/2014
Luogo di pubblicazione: Berlin Heidelberg
Abstract: In the past, formal verification of security properties of distributed applications has been mostly targeted to security protocols and generic security properties, like confidentiality and authenticity. At ESSOS 2010, Moebius et. al. presented an approach for developing Java applications with formally verified application-specific security properties. That method, however, is based on an interactive theorem prover, which is not automatic and requires considerable expertise. This paper shows that a similar result can be achieved in a fully automated way, using a different model-driven approach and state-of-the-art automated verification tools. The proposed method splits the verification problem into two independent sub-problems using compositional verification techniques and exploits one tool for analyzing the security protocol under active attackers and another tool for verifying the application logic. The same case study that was verified in the previous work is used here in order to show how the new approach works
Data: 2014
Status: Pubblicato
Lingua della pubblicazione: Inglese
Parole chiave: security protocols, security-aware applications, formal methods, formal verification, model-driven development, model checking
Dipartimenti (originale): DAUIN - Dipartimento di Automatica Informatica
Dipartimenti: DAUIN - Dipartimento di Automatica e Informatica
URL correlate:
Area disciplinare: Area 09 - Ingegneria industriale e dell'informazione > SISTEMI DI ELABORAZIONE DELLE INFORMAZIONI
Data di deposito: 19 Feb 2016 10:34
Data ultima modifica (IRIS): 19 Feb 2016 09:34:03
Data inserimento (PORTO): 21 Feb 2016 03:35
Numero Identificativo (DOI): 10.1007/978-3-319-04897-0_4
Permalink: http://porto.polito.it/id/eprint/2521101
Link resolver URL: Link resolver link
Citazioni:

Il campo presenta il numero di citazioni presenti sulle banche dati Scopus e Web of Science e permette di accedere ai relativi record. Visualizza inoltre il link al record presente su Google Scholar.

Possono verificarsi discrepanze rispetto ai dati presenti sulle banche dati per i seguenti motivi:

  • Differenze tra i dati riportati su IRIS e quelli presenti nelle banche dati.
  • Il numero di citazioni riportate su PORTO viene estratto mensilmente. Il dato citazionale presente sulle singole banche dati è aggiornato in tempo reale
  • Il numero di citazioni per WoS viene calcolato sulla base delle collezioni in abbonamento (Science citation index Expanded e Conference Proceedings Citation Index)

Per informazioni o segnalazioni contattare scrivia/porto

+
-

Azioni (richiesto il login)

Visualizza il documento (riservato amministratori) Visualizza il documento (riservato amministratori)