SWEN90010 – High Integrity
Systems Engineering Lecture 1: Introduction
Toby 2, Melbourne Connect
http://people.eng.unimelb.edu.au/tobym @tobycmurray
Copyright By PowCoder代写 加微信 powcoder
ADMINISTRIVIA
Monday 10am (Zoom, for now) Thursday 10am (Zoom, for now)
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Pengbo Cheung
in-person and online
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Subject Notes (on LMS) Booklet:
A living resource. Will be updated as we go.
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Lecture Slides
Assignments
3 Assignments, comprise 50% of your grade for the subject
Hurdle: 25/50 for your assignments overall (Exam Hurdle: 25/50 for the written exam)
Rough Timeline
(might change slightly as we go)
1. ~10 marks, released Week 2, due Week 4 (~2 wks) 2. ~20 marks, released Week 5, due Week 7 (~3 wks) 3. ~20 marks, released Week 8, due Week 11 (~3 wks)
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Group Work
Assignments you will do in self-selected pairs
This week: choose your pair and enter your student numbers here:
https://forms.office.com/r/f69FJF6EMQ
On Monday Week 2 we will allocate any remaining students who have not filled in the above form.
7 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Discussion Board
Don¡¯t reveal information about your own assignment solutions here.
Do answer others¡¯ questions.
8 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Academic Integrity
https://academichonesty.unimelb.edu.au/
The University misconduct policy applies.
Students are encouraged to discuss the assignment topics, but all submitted work must represent the pair¡¯s understanding of the topic.
We take academic misconduct very seriously. In this subject in the past, we have successfully prosecuted several students that have breached the university policy. Often this results in receiving 0 marks for an assignment, and in some cases has resulted in failing the subject.
HIGH INTEGRITY SYSTEMS ENGINEERING
Engineering vs Programming Programming
December 2009:
– Data breach, exposing 32 million+ user accounts. – Including plaintext user passwords
– Unpatched ten-year-old SQL vulnerability.
– Failed to notify users
– Miscommunicated the extent of the breach.
11 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Equifax Breach
US Credit Bureau
May – July 2017
140 million records exposed
209,000 US credit card numbers exposed, etc.
Exploited a web app vuln that had been patched months earlier
12 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Engineering
Methods for making large-scale
software that is fit for purpose Criteria Methods
Performance Reliability Design Testing
Correctness Requirements analysis
Usability Scalability
Time to market Development cost
(code, design, requirements)
Prototyping
High Integrity Systems
How are these different from ordinary software systems?
¡°must work right the first time¡±
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
High Integrity Systems
Ones in which failure has unacceptable consequences
Loss of life
Loss of money Environmental damage Loss of mission Loss of privacy
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
A Thought Experiment
Would you fly on a plane whose software was written by a web developer?
Why do you trust flight software? What do those engineers do differently?
What this subject is about.
Safety Critical Systems
Obvious ones:
Network-enabled Pacemakers Software in Car ECUs Railway Signalling
Less obvious ones:
Ambulance dispatch system
17 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Security Critical Systems
Almost everything, as incentives improve for attackers
as more things of value become network accessible Computer systems at your GP¡¯s clinic or hospital
Email servers of DNC
18 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Finance Critical Systems
Obvious ones:
High-Frequency Trading Software Stock Exchange Banking
Less obvious ones:
Hosting providers
19 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Mission Critical
Think NASA
20 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
High Integrity Engineering
Old London Bridge, 1632
21 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
London Bridge today
Safety and Security Analysis
Hazard analysis and fault prediction
22 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Engineers in established fields use applied mathematics to predict the behavior and properties of their designs with great accuracy. Software engineers, despite the fact that their creations exhibit far more complexity than physical systems, do
not generally do this . . .
[T]he applied mathematics of software is formal logic,
and calculating the behavior of software is an exercise
in theorem proving. Just as engineers in other disciplines need the speed and accuracy of computers to help them perform their engineering calculations, so software engineers can use the speed and accuracy of computers to help them prove the . . . theorems required to predict the behavior of software.
. Formal methods and critical systems in the real world Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Formal Methods
Formal Methods
Software Engineering
Requirements
Implementation
Formal Methods
Properties
Design Model
Hoare Logic SPARK
Code Semantics
24 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Small trustworthy foundation
microkernel with verified functional correctness, plus verified integrity and confidentiality enforcement
High assurance components in presence of other components
Apps Legacy App.
Legacy App.
Linux Server
Sensitive App
Trusted Service
IPC Threads VM
IRQ Capabilities
25 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Properties
Design Model
Code Semantics
Confiden- tiality
Availability
Abstract Model
C Imple- mentation
Binary code
Open source and proofs:
https://seL4.systems
26 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Proof Proof Proof
Trustworthy Systems |
Trustworthy Systems |
Cost of Formal Methods
Make predictions about system behaviour
Reason about low-level attacks
Properties
Design Model
Code Semantics
29 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
More Expensive
Is it worth it?
For high-assurance domains, definitely. (space, aviation, Defence, etc.)
In these domains there is no cheaper way to develop software.
For others, incentives not quite right yet.
30 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Commercial Formal Methods
31 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Course Outline
Loosely based around Altran¡¯s development model But not using all of their toolset
Safety/Security Analysis Design Modelling and Analysis (Alloy)
(Hoare Logic) & Safe Languages (SPARK)
Fault Tolerant Design
32 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
One more thing
Interested in learning a theorem prover?
You won¡¯t get any course credit, although what you learn will be useful for this course.
33 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com