School of CSE - Details Needed for New Course Proposal

Course Title: High Assurance Computing with Advanced Languages

Proposer: Manuel Chakravarty

Rationale
Why is the new course being proposed?

  Many courses cover good development practices based on a solid engineering
  discipline (eg, COMP2041 and COMP3141/4003).  However, it is virtually
  impossible to get beyond a certain level of assurance with these techniques
  alone (eg, Evaluation Assurance Levels of the Common Criteria, ISO/IEC
  15408, beyond EAL4 are generally assumed to be out of reach).  We also have
  courses that cover specific formal methods and associated tools (eg,
  COMP4151, COMP4161, and COMP9116) as means to achieve high assurance.

  We are lacking any coverage of programming language technology to achieve
  high levels of assurance, despite such methods already being used in
  industry (eg, Intel, Galois Connections, Linspire, Ericsson).  The change of
  the first-year curriculum to more low-level languages and programming is
  doing its share to increase this lack.  The proposed course will fill the
  current gap in our curriculum.

What are the academic objectives?

  Students will understand and be able to apply programming language
  technology to improve the trust that can be placed in software components.
  Specifically, they will learn about

  * advanced type systems,
  * formal reasoning about functional programs,
  * encapsulation of side effects,
  * specification-based test generators,
  * domain specific languages, and
  * prototyping for high-assurance.

Which programs/stage does it serve?

  4 year

Why can the same objectives not be achieved with existing courses?

  They do not cover the necessary material.

How does the proposed course relate to other courses?

  Relationship to COMP2041 and COMP3141/4003: These courses cover standard
    engineering practices (roughly corresponding to EAL1-4).  The proposed
    course covers techniques needed to go beyond that (e.g., EAL5 upwards).

  Relationship to COMP4151 and COMP9116: These courses cover specific formal
    methods and associated tools, but do not cover the use of very high-level
    languages (and in particular advanced type systems) to achive high
    assurance.

What overlap is there?
If there is any overlap, why is this justified/not a problem?

  * No significant overlap with COMP4151, as COMP4151 focuses on model
    checking.
  * No significant overlap with COMP4161, as COMP4161 focuses on theorem
    proving technology.
  * No significant overlap with COMP9116, as COMP9116 focuses on state
    transformers and the B method.
  * COMP3161/COMP9161 discusses type systems, but does so from the perspective
    of fundamental concepts of programming languages and programming language
    semantics.  It also only covers a basic feature set.

  In summary, there is no significant overlap with any existing course.

Stakeholders and Consultation
Who are the potential stakeholders, who was consulted about the
proposal (inside the School as well as outside), what was the
result of that consultation?

  I spoke to the lecturers of other language-related courses, namely
  COMP3131/COMP9102 and COMP3161/COMP9161, and the academics of the
  Programming Languages and Compilers research group.  They support
  the present proposal.

  I also discussed the proposal with the NICTA Formal Methods and ERTOS
  groups who have an interest in the material of the proposed course and,
  in particular, have U/G and P/G students that would benefit from the 
  proposed course.  They also support the proposal.

Enrolment Impacts
Likely enrolment (with justification), and impact on enrolments of
other courses.

  * 25
  * I don't expect any specific impact of enrollment in other courses.

Justification of Prerequisites (or lack thereof)

  COMP3161/COMP9161 could be a prerequisite (and this would avoid a minor
  duplication of material), but considering the amount of overlap and the
  likely impact on enrollment, it seems not to be justified.

Any Courses this is Replacing, and Why?

  N/A

Delivery and Assessment
Anything noteworthy about delivery mode, assessment (with justification).

  Standard (lectures with assignments and final exam).

Handbook Entry

  Trust in the safety and security of software systems is increasingly
  important with the use of software in systems where failure or sabotage can
  lead to loss of life or be very expensive (this includes medical and
  financial applications as well as software use for power grids, mass
  transport systems, and security infrastructure).  This courses covers
  language-based safety and security engineering techniques including advanced
  type systems, formal reasoning, encapsulation of side effects,
  specification-based test generators, domain specific languages, and
  prototyping for high-assurance.  It demonstrates at concrete examples how
  modern functional languages are used to achieve high assurance and conveys
  hands on experience by practical assignments.

Textbooks/References

  There is no textbook that covers the entire material (or at least most of
  it).  Hence, the material will be drawn from individual book chapters and
  research papers.  I will tie this together in lecture notes for the benefit
  of the students.

Syllabus
Indicative syllabus / overview of contents (at a level of detail
well beyond that of the handbook entry)

  Contents [12 weeks payload]:
  * Advanced type systems I [3 weeks]
    - Parametric polymorphism and ad-hoc polymorphism
    - Existential types
    - Regular data types
    - Higher-orderness
    - Singleton types
    - Phantom types
    - Generalised algebraic data types
  * Formal reasoning [2 weeks]
    - FunMath
    - Formal statements about programs
    - Equational reasoning
    - Program derivations
  * Advanced type systems II [3 weeks]
    - Encoding properties in types
    - Indexed type families
    - Dependent types
    - Proof carrying code and typed assembly language
  * Purity [1 week]
    - Clearly delimited impact of modifications, no race conditions etc
    - Isolation of side effects
    - Isolation of I/O
    - Encapsulated state
  * Tools [1 weeks]
    - QuickCheck and the new coverage checker from Galois
    - Language-oriented support by theorem provers
  * Domain specific languages [1 week]
    - Case study: Cryptol
  * Prototyping [1 week]
    - Case study: seL4

Effect on School Resources:

1. Who is proposed to teach the proposed new course,
   and what impact would this have on their planned/current allocation?

  Manuel Chakravarty, and this has already been discussed with Jingling Xue
  for the teaching allocation of 2007, Session 2.

2. What sort of tutorial component is proposed, if any?

  None.

3. What is the likely impact on lab utilisation (this relates
   to assignment and project work as well as scheduled labs?

  Standard.

4. Any other resource needs? E.g. special print/disk quota, access to
   servers, access to special machines, special labs.

  N/A