HIS - Summary High Integrity Systems Engineering PDF

Preview

Summary

An outline for the field of examination....

Description

The University of Melbourne SWEN90010: High Integrity Systems Engineering Learning Outcomes By the end of this subject, a student should be able to do the following (categorised by chapters in the course notes): Chapter 1 — An Introduction to HISE 1. Define the term “high-integrity system” High integrity systems a software-controlled system in which, in the event they fail, could result in harm to humans (including loss of life), harm on the environment, mass destruction of property, or harm to society in general. 2. Define the different classes of high-integrity system I. Safety-critical systems: Systems whose failure may result in harm to humans or the environment. Examples include aerospace systems, medical devices, automotive systems, power systems, and railway systems. II. Security-critical systems: Systems whose failure may result in breach of security. Examples in- clude defence systems, government data stores. III. Mission-critical systems: Systems whose failure may result in the failure of some deliberative missions. Examples include navigation systems on autonomous aerospace vehicles, computer- aided dispatch systems (e.g. in emergency services), and command-andcontrol systems in armed forces. IV. Business-critical systems: Systems whose failure may result in extreme financial loss to a business or businesses. Examples include stock exchange systems, trade platforms, and even accounting systems (e.g. in a bank). Chapter 2 — Ada 1. Describe the features of Ada that make it suitable for high-integrity software Ada is already much “safer” than C; better encapsulation. stronger type system, more static guarantees. more runtime checks 2. Read and modify basic Ada programs Chapter 3 — Safety engineering 1. Explain the role of safety engineering in the system engineering lifecycle. I. Requirements Analysis and Product Definition II. Design and Implementation Phases III. Safety Cases

2. Discuss the role of accidents and incidents in the safety analysis process Safety engineers are experts in past accidents, incidents and failures. They study past accident causes to determine hazards for new systems. Then design the system to be safe in the face of these things, reducing the chance of accidents happening. 3. Perform a preliminary hazard analysis using the HAZOP method

4. Apply the fault-tree analysis method to a system for a given fault

Chapter 4 — Model-based specification 1. Explain the advantages and disadvantages of formal model-based specification in software engineering Pros: Cons: 1) Small 1) Requires specialised 2) Unambiguous expertise 3) Abstract from Might lengthen time to Implementation implementation Loads more 4) Machine-Checkable effort early in the 5) Forces thinking up-front development process 6) Gets mistakes out of the 2) Not necessarily well suited way early (i.e. when they to projects with rapidly are cheaper to fix) changing requirements. 2. Apply basic logic, set/relational theory concepts to softwarebased problems 3. Model a domain using the Alloy language 4. Define and check assertions using the Alloy language and tool 5. Model and reason about (properties of) execution sequences in Alloy Chapter 5 — Fault-tolerant design 1. Explain the concept of fault tolerance in systems engineering A system is said to be fault tolerant if it can continue to function according to its specification in the presence of a finite number of faults. 2. Compare hardware and software fault tolerance Hardware (tends to) fail randomly

Software (tends to) fail systematically

3. Design, analyse, and critique a fault-tolerant hardware design 4. Design, analyse, and critique a fault-tolerant software design 5. Implement algorithms for majority voting, median voting, and kplurality voting 6. Compare and contrast the different voting algorithms, and evaluate their use in specific systems I. Majority voting: the output is the value on which more than half of the components agree. II. Generalised k-plurality voting: A k-plurality voter can be used to raise (increase k) or lower (decrease k) the risk tolerance of a system. III. Generalised median Voting simply chooses the median value by continually removing the elements n and m For example, if the outputs from all components are correct and sufficiently equal (the first row of the table), then all three voters will produce a correct output. However, if a majority of the outputs are incorrect and none are sufficiently equal (fifth row), then the majority and k-plurality voters will each produce no output, while the median voter will produce an incorrect output. 7. Apply the concepts of duplication, parity coding and checksums to small information redundancy problems, and explain the situations in which cryptographic mechanisms are necessary instead. 8. Analyse and explain the lower bounds for Byzantine Agreement in the authenticated and unauthenticated models, and the protocols that achieve those bounds. Chapter 6 — SPARK 1. Describe the features of SPARK that make it suitable for highintegrity software SPARK removes many of the features of Ada that are unconsidered either unsafe, or difficult to verify. These include language features such as: • Dynamic memory allocation • Tasks • Gotos • Exceptions • Generics • Access types (similar to references in other languages) • Recursion Chapter 8 — Reasoning about program correctness

1. Explain the advantages and disadvantages of program proof compared to other program verification techniques. Program differs from what was proved. (proofs are always over mathematical models) 2. Explain the meaning of Hoare logic statements: {P } S {Q} This states that, if we can establish that {P} S {Q} is true, then any precondition that is at least as strong as P, and any postcondition that is at least as weak as Q, are also valid preconditions/postconditions for the program S. 3. Devise appropriate loop invariants for reasoning about loops using Hoare logic 4. By hand, prove the correctness or otherwise of small programs using Hoare logic Rule of Assignment:

Rule of Consequence:

Generalised Assignment Rule:

Rule of Sequencing:

Conditional Rule:

Iteration Rule:

Chapter X — Security and cryptography 1. Informally describe the main security properties of digital signatures, message authentication codes, and cryptographic hash functions.

2. Understand and analyse the logical trust structure of digital certificates or the properties of public key encryption and synthesise a model of it in Alloy. 3. Recall and explain some specific recent examples of security problems caused by the use of weak or poorly implemented cryptography. They left the corresponding private key sitting weakly encrypted on every computer Someone cracked it, so now any affected Lenovo making an SSL/TLS connection could be intercepted by anyone (even externally) The Superfish CA was trusted for anything: SSL/TLS certificates, code, etc. “Armed with the private key and its password, you can now sign websites and even software in a way that any affected Lenovo user will trust. 4. Explain at a high level how the Bitcoin protocol works and how certain properties are achieved. • Hash (using SHA-256) o The prior block o The transactions in the block being added o A randomly-chosen nonce n • Succeed when the digest (i.e. output of SHA-256) is below some threshold o This proves you tried a lot of different n values.  You make money, “mine bitcoins” as a result – the transactions list the reward

o The threshold necessary decreases as more participants join the network • Broadcast the new block, including n o This now added to the blockchain o It took a long time to generate, but anyone can test it...