Affiliations: [a] Dipartimento di Matematica, Università di Padova, Via Trieste, 63 35121 Padova, Italy. baldan@math.unipd.it | [b] DAIS, Università Ca’ Foscari Venezia, Dorsoduro 3246 - 30123 Venezia, Italy. acarraro@dsi.unive.it
Note: [*] Work supported by the project Récré (ANR) and the MIUR PRIN project CINA.
Note: [†] Address for correspondence: Dipartimento di Matematica, Università di Padova, Via Trieste, 63 35121 Padova, Italy
Abstract: The concept of non-interference has been introduced to characterise the absence of undesired information flows in a computing system. Although it is often explained referring to an informal notion of causality - the activity involving the part of the system with higher level of confidentiality should not cause any observable effect at lower levels - it is almost invariably formalised in terms of interleaving semantics. Here we focus on Petri nets and on the BNDC (Bisimilarity-based Non-Deducibility on Composition) property, a formalisation of non-interference widely studied in the literature. We show that BNDC admits natural characterisations based on the unfolding semantics - a classical true concurrent semantics for Petri nets - in terms of causalities and conflicts between high and low level activities. This leads to algorithms for checking BNDC on various classes of Petri nets, based on the construction of suitable complete prefixes of the unfolding. We also developed a prototype tool UBIC (Unfolding-Based Interference Checker), working on safe Petri nets, which provides promising results in terms of efficiency.
Keywords: Petri nets, non-interference, bisimilarity-based non-deducibility on composition (BNDC), unfolding, true concurrency, verification
