CS代写 SWEN90010 – High Integrity

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