Affiliations: [a] Department of Philosophy, University of Milan, Via Festa del Perdono 7, 20122, Milan, Italy. E-mail: [email protected] | [b] Department of Computer Science, Middlesex University, the Burroughs, NW4 4BT, London, United Kingdom. E-mail: [email protected]
Abstract: Software management systems need to preserve integrity by the handling, approval, tracking and execution of changes on the packages of the current installation profile. This is a problematic task, which needs to be accounted for both in terms of installation of new packages and removal of conflicting ones. While existing approaches are able to identify dependency satisfaction and conflicts, a broader and efficient approach can be formalised in terms of trust. Positive instances of trust are required by the identification of safely installable packages. Negative trust, a much less explored concept, can be useful to analyse the complementary issue of packages’ removal both in case of conflicts and of security issues. In this paper we develop a logic of negative trust with two aims: identifying packages that are undesirable in view of the current installation profile; and currently installed packages that become inconsistent with a new intended installation. The logic provides distinct procedures for the identification of either case. We illustrate properties of the calculus, provide a simple working example and offer a translation of the protocol to the Coq proof assistant for verification of its formal correctness.
