Building a safety case is a common approach to make expert judgement explicit about safety of a system. The issue of confidence in such argumentation is still an open research field. Providing quantitative estimation of confidence is an interesting approach to manage complexity of arguments. This paper explores the main current approaches, and proposes a new model for quantitative confidence estimation based on Belief Theory for its definition, and on Bayesian Belief Networks for its propagation in safety case networks.
In @cite_26 , the inventors of GSN address the confidence issue, by proposing to split a traditional safety case in two pieces. The first is the safety argument, showing all evidences, and the second is a confidence argument that addresses confidence in evidences, contexts, and individual inferences. This confidence argument is also represented with GSN. It starts by adding to the safety case some possible uncertainty sources, which are called Assurance Claim Points (ACP), that are attached to inferences (the arrows connecting claims), contexts (explanatory information), or solutions. Then, for each ACP, an argumentation mainly focuses on demonstrating that the ACP is trustworthy and appropriate, which is built using GSN. Another proposal @cite_7 , is based on the ACP but only focuses on Context and Solution elements. The authors propose to use a map (Common Characteristic Map) as a check list to identify sources of uncertainties, with recursive dependencies. For instance, if a safety case includes a solution which is a "Process result", they propose the generic uncertainties related to "the use of a language", "the use of a tool", "the use of a mechanism", "the involved artifacts", etc. All those characteristics are then refined, with possible recursive dependencies.
@cite_26 @cite_7
2170178247 2626217303
We present AdvoCATE, an Assurance Case Automation ToolsEt, to support the automated construction and assessment of safety cases. In addition to manual creation and editing, it has a growing suite of automated features. In this paper, we highlight its capabilities for (i) inclusion of specific metadata, (ii) translation to and from various formats, including those of other widely used safety case tools, (iii) composition, with auto-generated safety case fragments, and (iv) computation of safety case metrics which, we believe, will provide a transparent, quantitative basis for assessment of the state of a safety case as it evolves. The tool primarily supports the Goal Structuring Notation (GSN), is compliant with the GSN Community Standard Version 1, and the Object Modeling Group Argumentation Metamodel (OMG ARM). We present a novel approach to proving the absence of timing channels. The idea is to partition the programâ s execution traces in such a way that each partition component is checked for timing attack resilience by a time complexity analysis and that per-component resilience implies the resilience of the whole program. We construct a partition by splitting the program traces at secret-independent branches. This ensures that any pair of traces with the same public input has a component containing both traces. Crucially, the per-component checks can be normal safety properties expressed in terms of a single execution. Our approach is thus in contrast to prior approaches, such as self-composition, that aim to reason about multiple (kâ � 2) executions at once. We formalize the above as an approach called quotient partitioning, generalized to any k-safety property, and prove it to be sound. A key feature of our approach is a demand-driven partitioning strategy that uses a regex-like notion called trails to identify sets of execution traces, particularly those influenced by tainted (or secret) data. We have applied our technique in a prototype implementation tool called Blazer, based on WALA, PPL, and the brics automaton library. We have proved timing-channel freedom of (or synthesized an attack specification for) 24 programs written in Java bytecode, including 6 classic examples from the literature and 6 examples extracted from the DARPA STAC challenge problems.