Security of software systems has to be preserved while they grow and change incrementally. The problem is to make the analysis of their security properties adhere to such a development. In particular we concentrate here on static type systems. Given a non-incremental type system, the algorithm we propose permits using it incrementally, so avoiding to develop new incremental versions of it. As a proof-of-concept we show how our technique permits an incremental checking of non-interference with robust declassification, starting from the classical type system by Myers, Sabelfeld and Zdancewic.

Robust Declassification by Incremental Typing

Galletta L.
2019

Abstract

Security of software systems has to be preserved while they grow and change incrementally. The problem is to make the analysis of their security properties adhere to such a development. In particular we concentrate here on static type systems. Given a non-incremental type system, the algorithm we propose permits using it incrementally, so avoiding to develop new incremental versions of it. As a proof-of-concept we show how our technique permits an incremental checking of non-interference with robust declassification, starting from the classical type system by Myers, Sabelfeld and Zdancewic.
2019
978-3-030-19051-4
978-3-030-19052-1
File in questo prodotto:
File Dimensione Formato  
festschrift_main.pdf

non disponibili

Tipologia: Documento in Post-print
Licenza: Nessuna licenza
Dimensione 547.32 kB
Formato Adobe PDF
547.32 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

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/20.500.11771/12759
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
social impact