1 Introduction

Assurance cases (ACs) are structured arguments, supported by evidence, intended to demonstrate that a system meets its requirements, such as safety or security, when applied in a particular operational context [24, 30]. They are recommended by several international standards, such as ISO26262 for automotive applications. An AC consists of a hierarchical decomposition of claims, through appropriate argumentation strategies, into further claims, and eventually supporting evidence. Several AC languages exist, including the Goal Structuring Notation (GSN) [24], Claims, Arguments, and Evidence (CAE) [2], and the Structured Assurance Case Metamodel (SACM)Footnote 1 [30], a standard that unifies several notations.

AC creation can be supported by model-based design, which utilises architectural and behavioural models over which requirements can be formulated [30]. However, ACs can suffer from logical fallacies and inadequate evidence [20]. A proposed solution is formalisation in a machine-checked logic to enable verification of consistency and well-foundedness [28]. As confirmed by avionics standard DO-178C, the evidence gathering process can also benefit from the rigour of formal methods (FMs). However, it is also the case that (1) ACs are intended primarily for human consumption, and (2) that formal models must be validated informally [21]. Consequently, ACs usually combine informal and formal content, and so tools must support this. Moreover, there is a need to integrate several FMs [26], potentially with differing computational paradigms and levels of abstraction [22], and so it is necessary to manage the resulting heterogeneity [19].

Fig. 1.
figure 1

Overview of our approach to integrative model-based assurance cases

Full size image

Vision. Our vision, illustrated in Fig. 1, is a unified framework for machine-checked ACs with heterogeneous artifacts and integrated FMs. We envisage an assurance backend for a variety of graphical assurance tools [9, 30] that utilise SACM as a unified interchange format, and an array of FM tools provided by our Isabelle-based verification platform, Isabelle/UTP  [16, 17]. Our framework aims to improve existing assurance processes by harnessing formal verification to produce mathematically grounded ACs with guarantees of consistency and adequacy of the evidence. In the context of safety regulation, it can help with AC evaluation through machine-checking and automated verification.

Contributions. A first step in this direction is made by the contributions of this paper, which are: (1) Isabelle/SACM, an implementation of SACM in Isabelle [25], (2) a front-end for Isabelle/SACM called interactive assurance language (IAL), which is an interactive DSL for the definition of machine-checked SACM models, (3) a novel formalisation of Tokeneer [1] in Isabelle/UTP, (4) the verification of the Tokeneer security requirementsFootnote 2, and (5) the definition of an AC with the claims that Tokeneer meets its security requirements. Our Tokeneer AC demonstrates how to integrate formal artifacts, resulting from Isabelle/UTP (4), and informal artifacts, such as the Tokeneer documentation.

Isabelle provides a sophisticated executable document model for presenting a graph of hyperlinked formal artifacts, like definitions, theorems, and proofs. It provides automatic and incremental consistency checking, where updates to artifacts trigger rechecking. Such capabilities can support efficient maintenance and evolution of model-based ACs [30]. Moreover, the document model allows both formal and informal content [32], and provides access to an array of automated proof tools [31, 32]. Additionally, Brucker et al. [4] extend Isabelle with DOF, a framework with a textual language for embedding of meta-models into the Isabelle document model, which we harness to embed SACM.

Isabelle/UTP [16, 17] harnesses Unifying Theories of Programming [22] (UTP) to provide formal verification facilities for a variety of languages, with paradigms as diverse as concurrency [13], real-time [14], and hybrid computation [15]. Moreover, verification techniques such as Hoare logic, weakest precondition calculus, and refinement calculus are all available through a variety of proof tactics. This makes Isabelle/UTP an obvious choice for modelling and verification of Tokeneer, and more generally as a platform for integrated FMs based on unifying semantics.

The paper is organised as follows. In Sect. 2 we outline preliminaries: SACM, Isabelle, and DOF. In Sect. 3 we describe the Tokeneer system. In Sect. 4 we begin our contributions by describing Isabelle/SACM, which consists of the embedding of SACM into DOF  (Sect. 4.1), and IAL (Sect. 4.2). In Sect. 5 we model and verify Tokeneer in Isabelle/UTP. In Sect. 6 we describe the mechanisation of the Tokeneer AC in Isabelle/SACM. In Sect. 7 we highlight related work, and in Sect. 8 we conclude.

2 Preliminaries

Fig. 2.
figure 2

Goal Structuring Notation

Full size image

SACM. ACs are often presented using a notation like GSN [24] (Fig. 2). Here, claims are rectangles, which are linked with “supported by” arrows, strategies are parallelograms, and the circles are evidence (“solutions”). The other shapes denote various types of context, which are linked to by the “in context of” arrows. SACM is an OMG standard meta-model for ACs [30]. It unifies, extends, and refines several predecessor notations, including GSN [24] and CAE [2] (Claims, Arguments, and Evidence), and is intended as a definitive reference model.

SACM models three crucial concepts: arguments, artifacts, and terminology. An argument is a set of claims, evidence citations, and inferential links between them. Artifacts represent evidence, such as system models, techniques, results, activities, participants, and traceability links. Terminology fixes formal terms for use in claims. Normally, claims are in natural languages, but in SACM they can also contain structured expressions, which allows integration of formal languages.

Fig. 3.
figure 3

SACM argumentation meta-model (See footnote 1)

Full size image

The argumentation meta-model is shown in Fig. 3. The base class is ArgumentAsset, which groups the argument assets, such as Claims, ArtifactReferences, and AssertedRelationships (which are inferential links). Every asset may contain a MultiLangString that provides a description, potentially in multiple natural and formal languages, and corresponds to contents of the shapes in Fig. 2.

AssertedRelationships represent a relationship that exists between several assets. They can be of type AssertedContext, which uses an artifact to define context; AssertedEvidence, which evidences a claim; AssertedInference which describes explicit reasoning from premises to conclusion(s); or AssertedArtifactSupport which documents an inferential dependency between the claims of two artifacts.

Both Claims and AssertedRelationships inherit from Assertion, because in SACM both claims and inferential links are subject to argumentation and refutation. SACM allows six different classes of assertion, via the attribute assertionDeclaration, including axiomatic (needing no further support), assumed, and defeated, where a claim is refuted. An AssertedRelationship can also be flagged as isCounter, where counter evidence for a claim is presented.

Fig. 4.
figure 4

Document model

Full size image

Isabelle. Isabelle/HOL is an interactive theorem prover for higher order logic (HOL) [25], based on the generic framework Isar [31]. The former provides a functional specification language, and an array of automated proof tools [3]. The latter has an interactive, extensible, and executable document model [32], which describes Isabelle theories. Plugins, such as Isabelle/HOL, DOF, Isabelle/UTP, and Isabelle/SACM have document models that contain conservative extensions to Isar.

Figure 4 illustrates the document model. The first section for context definition describes imports of existing theories, and keywords which extend the concrete syntax. The second section is the body enclosed between begin-end which is a sequence of commands. The concrete syntax of commands consists of (1) a pre-declared keyword (in ), such as the command , (2) a “semantics area” enclosed between , and (3) optional subkeywords (in ). Commands generate formal document artifacts. For example, the command creates a new theorem within the underlying theory context. When a document is edited by removal, addition, or alteration of formal artifacts, it is immediately executed and checked by Isabelle, with feedback provided to the frontend. This includes consistency checks for the context and well-formedness checks for the commands. Isabelle is therefore ideal for ACs, which have to be maintainable, well-formed, and consistent. In Sect. 4.2 we extend this document model with commands that define our assurance language, IAL.

Moreover, informal artifacts in Isabelle theories can be combined with formal artifacts using the command . It is a processor for markup strings containing a mixture of informal artifacts and hyperlinks to formal artifacts through antiquotations of the form . For example, mixes natural language with a hyperlink to the formal artifact through the antiquotation . This is important since antiquotations are also checked by Isabelle as follows: (1) whether the referenced artifact exists within the underlying theory context; (2) whether the type of the referenced artifact matches the antiquotation’s type.

DOF. A foundation for our work is DOF and its Isabelle Ontology Specification Language (IOSL) [4]: a textual language to model document classes, which extends the document model with new structures. We use the command from IOSL to add new document classes for each of the SACM classes. Instances of DOF classes sit at the meta-logical level, so they can be referenced using antiquotations, and carry an enriched version of Isabelle’s markup string.

Fig. 5.
figure 5

Tokeneer system overview

Full size image

3 Case Study: Tokeneer

To demonstrate our approach, we use the Identification Station (TIS)Footnote 3 illustrated in Fig. 5, a system that guards entry to a secure enclave. The pioneering work on the TIS assurance was carried out by Praxis High Integrity Systems and SPRE Inc. [1]. Barnes et al. performed security analysis, specification using Z, implementation in SPARK, and verification of the security properties. After independent assessment, Common Criteria (CC) Evaluation Assurance Level (EAL) 5 was achieved. Tokeneer is therefore a successful example of using FMs to assure a system against CC Though now more than fifteen years old, it remains an important benchmark for formal methods and assurance techniques.

The physical infrastructure consists of a door, fingerprint reader, display, and card (token) reader. The main function is to check the credentials on a presented token, read a fingerprint if necessary, and then either unlatch the door, or deny entry. Entry is permitted when the token holds at least three data items: (1) a user identity (ID) certificate, (2) a privilege certificate, with a clearance level, and (3) an identification and authentication (I&A) certificate, which assigns a fingerprint template. When the user first presents their token the three certificates are read and cross-checked. If the token is valid, then a fingerprint is taken, which, if validated against the I&A certificate, allows the door to be unlocked once the token is removed. An optional authorisation certificate is written upon successful authentication, which allows the fingerprint check to be skipped.

The security of the TIS is assured by demonstrating six Security Functional Requirements (SFRs) [7], of which the first three are shown below:

  • SFR1. If the latch is unlocked, then TIS must possess either a user token or an admin token. The user token must either have a valid authorisation certificate, or valid ID, Privilege, and I&A Certificates, together with a template that allowed to successfully validate the user’s fingerprint. Or, if the user token does not meet this, the admin token must have a valid authorisation certificate, with role of “guard”.

  • SFR2. If the latch is unlocked automatically by TIS, then the current time must be close to being within the allowed entry period defined for the User requesting access.

  • SFR3. An alarm will be raised whenever the door/latch is insecure.

Our objective is to construct a machine-checked assurance case that argues that the TIS fulfils these security properties, and integrate evidential artifacts from our mechanised model of the TIS behaviour in Isabelle/UTP.

4 Isabelle/SACM

Here, we encode SACM as a DOF ontology (Sect. 4.1), and use it to provide an interactive machine-checked AC language (Sect. 4.2). Our embedding implements ACs as meta-logical entities in Isabelle, rather than as formal elements embedded in the HOL logic, as this would prevent the expression of informal reasoning and explanation. Therefore, antiquotations to formal artifacts can be freely mixed with natural language and other informal artifacts.

4.1 Modelling: Embedding SACM in Isabelle

We embed the SACM meta-model in Isabelle using IOSL, and we focus on modelling Footnote 4 and its child classes from Fig. 3, as these are the most relevant classes for the TIS assurance argument that we develop in Sect. 6. The class has the following textual model:

figure p

Here, defines a new class, and automatically generates an antiquotation type, , which can be used to refer to entities of this type. is a class which inherits from, but is not discussed further. models the content association in Fig. 3. To model in Isabelle/SACM, we use DOF’s markup string. Thus, the usage of antiquotations is allowed for artifacts with the type .

  has three subclasses: (1) , which is a unified type for claims and their relationships; (2) , which is used to explicate the argumentation strategy being employed; and (3) , that evidences a claim with an artifact. Since DOF extends the Isabelle/HOL document model, we can use the latter’s types, such as sets and enumerations (algebraic datatypes), in modelling SACM classes, as shown below:

figure ac

Here, defines a HOL enumeration type, is the defined enumeration type, is the set type, and is the optional type. Attribute is of type , which specifies the status of instances of type . Examples of in SACM are claims, justifications, and both kinds of arrows from Fig. 2. The attribute is an association to the class , which is not discussed here. Finally, the attribute is an association to from the , allowing instances of type to be supported by evidential artifacts.

The class from Fig. 3 inherits from the class . This means that inherits the attributes , , and of type . The other child class of is:

figure az

This models the relationships between instances of type , such as the “supported by” and “in context of” arrows of Fig. 2. specifies whether the target of the relation is supported or refuted by the source, and is an association to , which models GSN strategies in SACM. The child classes of also have the attributes and , both of type .

4.2 Interactive Assurance Language (IAL)

IAL is our assurance language with a concrete syntax consisting of various Isabelle commands that extend the document model in Fig. 4. Each command generates SACM class instances and performs a number of checks: (1) standard Isabelle checks (Sect. 2); (2) OCL constraints imposed on the attributes by SACM (provided by DOF); (3) well-formedness checks against the meta-model, i.e. instances comply to the type restrictions imposed by the SACM datatypes.

IAL instantiates from Sect. 4.1 to create SACM models in Isabelle, for example, the command creates an instance of the class . Attributes and associations of a class have a concrete syntax represented by an Isabelle subcommand. For example, the association is represented by ; where is DOF’s markup string. A selection of IAL commands is given below.

figure br

creates an instance of type with an identifier , and content described by a . The antiquotation can be used to reference the created instance. The subcommands , and are optional. creates an inference between several instances of type . It has subcommands and that are both lists of antiquotations pointing to The use of antiquotations to reference the instances ensures that Isabelle will do the checks explained in Sect. 2. similarly asserts that an instance should be treated as context for another, and associates evidence with a claim. All instances created by IAL are semi-formal, since they can contain both informal content and references to formal content that are machine checked.

Fig. 6.
figure 6

Interactive DSL

Full size image

Figure 6 shows the interactive nature of IAL. It represents an inferential link between the semi-formal artifacts and . The semi-formal artifact , which is the inferential link between and , is created via the command . However, does not exist, and so the error message at the top is issued. The command is then used to reference using the antiquotation . This also leads to an error, shown at the bottom, since was not introduced to the context of the document model, due to the error at the top.

We have now developed Isabelle/SACM and our IAL. In the next section we consider the modelling verification of the Tokeneer system.

5 Modelling and Verification of Tokeneer

Here, we present a novel mechanisation of Tokeneer in Isabelle/UTP [16, 17] to provide evidence for the AC. In [7], the SFRs are argued semi-formally, but here we provide a formal proof. We focus on the verification of SFR1Footnote 5, the most challenging of the six SFRs, and describe the necessary model elements.

5.1 Modelling and Mechanisation

The TIS specification [6] describes an elaborate state space and a collection of relational operations. The state is bipartite, consisting of (1) the digital state and (2) the monitored and controlled variables shared with the real world. The TIS monitors the time, enclave door, fingerprint reader, token reader, and several peripherals. It controls the door latch, an alarm, a display, and a screen.

The specification describes a state transition system, illustrated in Fig. 7 (cf. [6, page 43]), where each transition corresponds to an operation. Several operations are omitted due to space constraints. Following enrolment, the TIS becomes quiescent (awaiting interaction). ReadUserToken triggers if the token is presented, and reads its contents. Assuming a valid token, the TIS determines whether a fingerprint is necessary, and then triggers either BioCheckRequired or BioCheckNotRequired. If required, the TIS then reads a fingerprint (ReadFingerOK), validates it (ValidateFingerOK), and finally writes an authorisation certificate to the token (WriteUserTokenOK). If the access credentials are available (waitingEntry), then a final check is performed (EntryOK), and once the user removes their token (waitingRemoveTokenSuccess), the door is unlocked (UnlockDoor).

Fig. 7.
figure 7

TIS main states

Full size image

We mechanise the TIS using hierarchical state space types, with invariants adapted from the Z specification [6]. We define the operations using guarded command language [10] (GCL) rather than the Z schemas directly, to enable syntax-directed reasoning. GCL has a denotational semantics in UTP’s relational calculus [22], so that it is possible to prove equivalence with the corresponding Z operations. We use a GCL variant that follows the following syntax:

Here, \(\mathcal {P}\) is a program, \(\mathcal {E}\) is an expression, and \(\mathcal {V}\) is a variable. The language provides sequential composition, guarded commands, non-deterministic choice, and assignment. We adopt a frame operator \(a:\!\![P]\), which states that P changes only variables in the namespace a [16, 17]. This enables modular reasoning about the TIS internal and real-world states, which is a further novelty of our work.

State Types. We first describe the state space of the TIS state machine:

We define state types for the TIS state, controlled variables, monitored variables, real-world, and the entire system, respectively. The controlled variables include the physical latch, the alarm, the display, and the screen. The monitored variables correspond to time (now), the door (door), the fingerprint reader (finger), the tokens, and the peripherals. RealWorld combines the physical variables, and SystemState composes the physical world (rw) and the TIS (tis).

Variable currentUserToken represents the last token presented to the TIS, and userTokenPresence indicates whether a token is currently presented. The variable status is used to record the state the TIS is in, and can take the values indicated in the state bubbles of Fig. 7. Variable issuerKey is a partial function representing the public key chain, which is needed to authorise user entry.

Operations. We now specify a selection of the operations over IDStationFootnote 6:

Each operation is guarded by execution conditions and consist of several assignments. BioCheckRequired requires that the current state is , the user token is , and sufficient for entry (UserTokenOK), but there is no authorisation certificate (\(\lnot UserTokenWithOKAuthCert\)). The latter two predicates essentially require that (1) the three certificates can be verified against the public key store, and (2) additionally there is a valid authorisation certificate present. Their definitions can be found elsewhere [6]. BioCheckRequired updates the state to and the display with an instruction to provide a fingerprint. UnlockDoorOK requires that the current state is , and the token has been removed. It unlocks the door, using the elided operation UnlockDoor, returns the status to , and updates the display.

These operations act only on the TIS state space. During their execution monitored variables can also change, to reflect real-world updates. Mostly these changes are arbitrary, with the exception that time must increase monotonically. We therefore promote the operations to SystemState with the following schema.

In Z, this functionality is provided by the schema UserEntryContext [6], from which we derive the name UEC. It promotes Op to act on tis, and composes this with a relational predicate that constrains the real-world variables (rw); this separation enables modular reasoning. The behaviour of all monitored variables other than now is arbitrary, and all controlled variables are unchanged. Then, we promote each operation, for example . The overall behaviour of the entry operations is given below:

In each iteration of the state machine, we non-deterministically select an enabled operation and execute it. We also update the controlled variables, which is done by composition with the following relational update operation.

This allows time to advance, allows other monitored variables to change, and copies the digital state of the latch and display to the corresponding controlled variables. The system transitions are described by .

5.2 Formal Verification of SFR1

We first formalise the TIS state invariants necessary to prove SFR1:

\(Inv_1\) states that whenever the TIS is in a state beyond , then either a valid authorisation certificate is present, or else the user token is valid; it corresponds to the first invariant in the IDStation schema [6, page 26]. \(Inv_2\) states that whenever in state or , then either an authorisation certificate or a valid finger print is present. \(Inv_2\) is actually not present in [6], but we found it necessary to satisfy SFR1Footnote 7. We elide the additional eight invariants that deal with administrators, the alarm, and audit data [6].

Unlike [6], which imposes the invariants by construction, we prove that each operation preserves the invariants using Hoare logic, similar to [27]:

Theorem 5.1

\({\{}\textit{TIS-inv} {\}}\, TISUserEntryOp \,{\{}\textit{TIS-inv} {\}}\)    

This theorem shows that the state machine never violates the 10 state invariants, and we can assume that they hold, to satisfy any requirements. This involves discharging verification conditions for a total of 22 operations in Isabelle/UTP, a process that is automated using our proof tactic .

We use this to assure SFR1, which is formalised by the formula FSFR1, that characterises the conditions under which the latch will become unlocked having been previously locked. We can determine these states by application of the weakest precondition calculus [10], which mirrors the (informal) Z schema domain calculations in [7, page 5]. Specifically, we characterise the weakest precondition under which execution of TISUserEntryOp followed by TISUpdate leads to a state satisfying . We formalise this in the theorem below.

Theorem 5.2

(FSFR1)

Proof

Automatic, by application of weakest precondition and relational calculus.

We conjoin the formula with to capture behaviours when the latch was initially locked. The only operation that unlocks the door for users is UnlockDoorOK, as confirmed by the calculated unlocking precondition:

that is, access is permitted and the token has been removed. We conjoin this with \(\textit{TIS-Inv}\), since we know it holds in any state. We show that this composite precondition implies that either a valid user token and fingerprint were present (using \(Inv_2\)), or else a valid authorisation certificate. We have now verified a formalisation of SFR1. In the next section we place this in the context of an AC.

Fig. 8.
figure 8

TIS claim formalization

Full size image

6 Mechanising the Tokeener Assurance Case

Here, we use Isabelle/SACM to model an AC with the claim that TIS satisfies SFR1, using Theorems 5.1 and 5.2 from Sect. 5 as evidential artifacts. The GSN diagram for the AC is shown in Fig. 8, which is inspired by the “formalisation pattern” [9]. Figure 8 is translated to IAL and the result is show in Figs. 9 and 10, which illustrate (1) a machine checked AC; (2) integration of informal, formal, and semi-formal artifacts; and (3) use of Isabelle/UTP verification techniques.

The Formalisation Pattern. [9] shows how results from a formal method can be used to provide evidence to an AC that claims to satisfy a given requirement {R}. The strategy used to decompose the claim “Informal requirement {R} is met by {S}” is contingent on the validation of both the formal model of {R} and the formal model of {S}. Consequently, the pattern breaks down the satisfaction of {R} into 3 claims stating that (1) the formal model of {S} is validated, (2) the formalisation of {R} correctly characterises {R}, and (3) the formal model of {S} satisfies the formalisation of {R}. The former two claims usually have an informal process argument. In Fig. 8, we adapt this pattern as follows. Firstly, instead of using two validation claims, we use two justification elements, and . This is to preserve the well-formedness of the AC – the “requirement validation” claims have a type different from the “requirement satisfaction” claims. An example of a “requirement satisfaction” claim is . Secondly, we add the “requirement satisfaction” claim for the state invariant of TIS.

In Fig. 8, we apply our adapted pattern to . This claim states that the informal requirement SFR1 is met, and references , with its natural language description, and the assumption . The latter is important, as the AC’s requirements are only satisfied when the invariant in Sect. 5 holds. is decomposed by the formalisation strategy, , which references the three formal artifacts (\(\textit{TIS-Inv}\)), and (TISUserEntryOp) from Sect. 5. This decomposition is contingent on the validation arguments expressed by and . The latter could be an explanation of how FSFR1 formalises SFR1, such as the description of Theorem 5.2 in Sect. 5. subclaims are and . The former is supported by the evidence which refers to Theorem 5.2, and the latter by which refers to Theorem 5.1.

Claims. Figure 9 shows the model of – from Fig. 8. In SACM, justifications, asusmptions, and claims are unified by the class . Thus, the claims and justifications from Fig. 8 are all represented by claims in Fig. 9. They are created using the command , with a name and content associated. Since the checks done by IAL are successful, no errors are issued.

Formal, Semi-formal, and Informal. The of the claims in Fig. 9 integrate hyperlinks, which are generated by antiquotations that reference semi-formal artifacts, i.e. instances created by IAL, formal artifacts, i.e. theorems and proof techniques created by Isabelle/HOL commands, and informal artifacts, i.e., natural language. For example, the of combines natural language with the antiquotation to insert a hyperlink to the formal artifact . Also, refers to the semi-formal artifact , and copies the natural language requirement from the Tokeneer documentation.

Fig. 9.
figure 9

TIS argument: claims and their relations in Isabelle/SACM

Full size image

Relations Between Claims. The strategy from Fig. 8, connecting the elements – , is modelled by in Fig. 9. is created using the command , which uses antiquotations to reference the premise claims , , and , i.e., the , and the conclusion claim , i.e., the . and are left undeveloped, and hence marked as : the argument should be completed later. Moreover, and are marked as , meaning that this argument is contingent on their satisfaction elsewhere.

Context. We model the relations between the context elements , , and the strategy from Fig. 8. This is done in Fig. 9 using the command which creates the relation . It uses antiquotations to connect with: (1) , which is an “SACM reference” to the artifact , which is created in Fig. 10 and models the verification tool; and (2) , . and , which are all artifact references to their corresponding artifacts created in Fig. 10 using . From the point of view of SACM, artifacts created using are references to the artifacts, and not the artifacts themselves. Similarly, relationships created using and link to artifact references.

Evidence. We model the relationships from Fig. 8 that link , to and respectively. This is done in Fig. 9 by and , which are created using the command . They support claims and by the “SACM references” and , respectively. One can see that and point to and using antiquotations. The latter are created in Fig. 10 using the command , which records an activity with a and . They also have a with antiquotations pointing to the formal artifacts and , which are Theorems 5.2 and 5.1, respectively. Also, the antiquotations and reference the formal artifacts and , which are Isabelle/UTP proof tactics.

Fig. 10.
figure 10

TIS argument: artifacts and their relations in Isabelle/SACM

Full size image

7 Related Work

Woodcock et al. [34] highlight defects of the Tokeneer SPARK implementation, indicate undischarged verification conditions, and perform robustness tests generated by the Alloy SAT solver [23] model. Using De Bono’s lateral thinking, these test cases go beyond the anticipated operational envelope and stimulate anomalous behaviours. In shortening the feedback cycle for verification and test engineers, theorem proving can help using this approach more intensively.

Despite its age, we see Tokeneer as a highly relevant benchmark specification, particularly since it is one of the grand challenges of the “Verified Software Initiative” [33]. As we have argued elsewhere [19], such benchmarks allow us to conduct objective analyses of assurance techniques to aid their transfer to other domains. The issues highlighted in [34] are systematic design problems that can be fixed by a change of the benchmark (e.g. by a two-way biometric identification on both sides of the enclave entrance). However, this is out of scope of our work and does not harm Tokeneer in its function as a benchmark.

Rivera et al. [27] present an Event-B model of the TIS, verify this model, generate Java code from it using the Rodin tool, and test this code by JUnit tests manually derived from the specification. The tests validate the model in addition to the Event-B invariants derived from the same specification, and aim to detect errors in the Event-B model caused by misunderstandings of the specification. Using Rodin, the authors verify the security properties (Sect. 3) using Hoare triples. Our work uses a similar abstract machine specification, but with weakest precondition as the main tool for the requirements. Beyond the replication of the Tokeneer case study, [27] deals with the relationship between the model and the code via testing, whereas we focus on the construction of certifiable assurance arguments from formal model-based specifications. Nevertheless, we believe Isabelle’s code generation features could be similarly applied.

We believe that our work is the first to put formal verification effort into the wider context of structured assurance argumentation, in our case, a machine-checked security case using Isabelle/SACM. We have also recently applied our technique to collision avoidance for autonomous robots [18]; a modern benchmark.

Several works bring formality to assurance cases [8, 9, 11, 29]. AdvoCATE is a powerful graphical tool for the construction of GSN-based safety cases [9]. It uses a formal foundation called argument structures, which prescribe well-formedness checks for the graph structure, and allow instantiation of assurance case patterns. Our work likewise ensures well-formedness, and additionally allows the embedding of formal content. Denney’s formalisation pattern [9] is an inspiration for our work. Our framework is an assurance backend, which complements AdvoCATE with a deep integration of modelling and specification formalisms.

Rushby shows how assurance arguments can be embedded into formal logic to overcome logical fallacies [29]. Our framework similarly allows reasoning using formal logic, but additionally allows us to combine formal and informal artifacts. We were also inspired by the work on evidential toolbus [8], which allows the combination of evidence from several formal and semi-formal analysis tools. Isabelle similarly allows integration of a variety of formal analysis tools [31].

8 Conclusions

We have presented Isabelle/SACM, a framework for computer-assisted assurance cases with integrated formal methods. We showed how SACM is embedded into Isabelle as an ontology, and provided an interactive assurance language that generates valid instances. We applied it to part of the Tokeneer security case, including verification of one of the security functional requirements, and embedded these results into a mechanised assurance argument. Isabelle/SACM enforces the usage of formal ontological links which represent the provenance between the assurance arguments and their claims, a feature inherited from DOF. Isabelle/SACM combines features from Isabelle/HOL, DOF, and SACM in a way that allows integration of formal methods and ACs [18].

In future work, we will connect Isabelle/SACM to a graphical AC tool, such as ACME [30], which will make the platform more accessible. We will consider the integration of AC pattern execution [9], to facilitate AC production. We will also complete the mechanisation of the TIS security case, including the overarching argument for how the formal evidence can satisfy the requirements of CC [5]. In parallel, we are developing our verification framework, Isabelle/UTP [16, 17] to support a variety of software engineering notations. We recently demonstrated formal verification facilities for a statechart-like notation [12, 13], and are also working towards tools to support hybrid dynamical languages [15] like Modelica and Simulink. Our overarching goal is a comprehensive assurance framework supported by a variety of integrated formal methods in order to support complex certification tasks for cyber-physical systems such as autonomous robots [18, 19].