Formal verification encapsulates the process of ensuring the correctness of systems withrespect to user-specified requirements, expressed as formal properties. This dissertation explores the different aspects of the verification of systems involving uncertainty, specified at an abstract level as Markov models, against system-level specifications, expressed as hyperproperties.In this context, we refer to models as frameworks used to capture the behaviour of systemswhile abstracting away the exact details of its inner workings. Such system models are rarely deterministic e.g., we may choose to simplify or remove elements that are irrelevant to the verification, we might not be aware of exact details of certain components in the system, or we might not be able to observe every aspect of the system. To this end, we chose to represent systems as Markov models due to their flexibility in representing uncertainty (in terms of nondeterminism, randomization, and partial observability), and its simplicity in using the current state to determine the future evolution of the system.The current ubiquitous nature of software demands verification of not only its isolatedbehaviours, but also ones relating to security, privacy, robustness, and efficiency. These additional requirements are more challenging to verify as they require simultaneous rea- soning across multiple system behaviours. Such requirements can be formally specified as hyperproperties. Prominent examples include noninterference of secret inputs on publicly observable outputs, observational determinism of public outputs, optimal path planning in robotics, individual fairness in models, side-channel timing attacks, conformance of different system versions, etc.Given this combination of model and properties, we explore the following:• We explored the parameter synthesis problem and developed an SMT-based solutionfor synthesizing values for unknown or missing parameters of the system, under the assumption of satisfaction of a given specification.• We generalize the probabilistic hyperlogic HyperPCTL by extending it to formally specifyrequirements involving nondeterministic choices and rewards in models. We discuss the expressive power of this extended logic, and how it makes the model checking problem for this logic undecidable, in general.• To provide tractable solutions to the model checking problem, we focused on a decidablefragment of HyperPCTL with a single existential quantifier and proposed an SMT- encoding-based model checking algorithm.• We identify two different fragments of HyperPCTL based on their ability to express thereachability requirement in most of our applications. For these two different fragments, we provide a randomized convex addition of a scheduler and a distribution-based ap- proach respectively.• We have developed prototypical implementations for each of the proposed algorithms.Specifically, to model check the nondeterministic and reward property extensions, we have built a tool HyperProb, which implements our SMT-based algorithm to sym- bolically model check restricted fragments of HyperPCTL.• To tackle the challenges of scalability, we explored statistical model checking as a pos-sible solution to model check a fragment of HyperPLTL and extended the tool PLASMA to evaluate our theory.
Read
