The use analysis and verification techniques based on formal methods to provide theoretical proof of security properties either in software, hardware and algorithm design.
The subdomains for this knowledge domain are:
- Formal specification of various aspects of security (e.g properties, threat models, etc.)
- Formal specification, analysis, and verification of software and hardware
- Information flow modelling and its application to confidentiality policies, composition of systems, and covert channel analysis
- New theoretically-based techniques for the formal analysis and design of cryptographic protocols and their applications
- Formal verification of security assurance
- Cybersecurity uncertainty models
- Cybersecurity concepts, definitions, ontologies, taxonomies, foundational aspects