Our goal is to provide different semiring-based formal tools for the specification of security requirements: we quantitatively enhance the open-system approach, according to which a system is partially specified. Therefore, we suppose the existence of an unknown and possibly malicious agent that interacts in parallel with the system. Two specification frameworks are designed along two different (but still related) lines. First, by comparing the behaviour of a system with the expected one, or by checking if such system satisfies some security requirements: we investigate a novel approximate behavioural-equivalence for comparing processes behaviour, thus extending the Generalised Non Deducibility on Composition (GNDC) approach with scores. As a second result, we equip a modal logic with semiring values with the purpose to have a weight related to the satisfaction of a formula that specifies some requested property. Finally, we generalise the classical partial model-checking function, and we name it as quantitative partial model-checking in such a way to point out the necessary and sufficient conditions that a system has to satisfy in order to be considered as secure, with respect to a fixed security/functionality threshold-value.

Semiring-based Specification Approaches for Quantitative Security

F Martinelli;I Matteucci;F Santini
2015

Abstract

Our goal is to provide different semiring-based formal tools for the specification of security requirements: we quantitatively enhance the open-system approach, according to which a system is partially specified. Therefore, we suppose the existence of an unknown and possibly malicious agent that interacts in parallel with the system. Two specification frameworks are designed along two different (but still related) lines. First, by comparing the behaviour of a system with the expected one, or by checking if such system satisfies some security requirements: we investigate a novel approximate behavioural-equivalence for comparing processes behaviour, thus extending the Generalised Non Deducibility on Composition (GNDC) approach with scores. As a second result, we equip a modal logic with semiring values with the purpose to have a weight related to the satisfaction of a formula that specifies some requested property. Finally, we generalise the classical partial model-checking function, and we name it as quantitative partial model-checking in such a way to point out the necessary and sufficient conditions that a system has to satisfy in order to be considered as secure, with respect to a fixed security/functionality threshold-value.
2015
Istituto di informatica e telematica - IIT
modal logic
partial model checking
Quantitative security
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/20.500.14243/305018
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact