Course Length:

20 hours over 10 weeks (1 two-hour meeting per week)

Course Description:

Formal methods for specifying security policies and systems requirements, and the verification of security properties. A hands-on course on methods for high-assurance using tools such as PVS/SAL, ACL2, and the NRL Protocol Analyzer. Prerequisite: COEN 253 (Secure Systems Development and Evaluation I).

Course Learning Objective:

Familiarity with techniques and tools for the specification and verification of systems and their security properties, to achieve high levels of assurance, with the goal of successful system evaluation under the Common Criteria.  Delves into the technical aspects of evaluation that are introduced in COEN 253. Provide hands-on experience with the use of contemporary tools for high-assurance.

Major Topics:

Formal security policy modeling.
Specification of system security functions.
Designing systems for verification and evaluation.
Verifying the correspondence of a system formal specification to a formal security policy model.
Protocol specification and verification.
Preparation of artifacts and evidence to meet Common Criteria evaluation requirements.

Method of Instruction:

Lectures, case studies, homework involving extensive tool interaction.

Evaluation Methods:

Tests, assignments, individual project writeups and presentations.