Modular Verification for Computer Security

For many software components, it is useful and important to verify their security. This can be done by an analysis of the software itself, or by isolating the software behind a protection mechanism such as an operating system kernel (virtual-memory protection) or cryptographic authentication (don�...

Full description

Saved in:
Bibliographic Details
Main Author: Appel, Andrew W.
Format: Conference Proceeding
Language:English
Subjects:
Authentication
Computer information security
Computer programs
Computer security
Cryptography
Foundations
Kernel
Kernels
Modularity
Radiation detectors
Safety
Software
verification
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:For many software components, it is useful and important to verify their security. This can be done by an analysis of the software itself, or by isolating the software behind a protection mechanism such as an operating system kernel (virtual-memory protection) or cryptographic authentication (don't accepted untrusted inputs). But the protection mechanisms themselves must then be verified not just for safety but for functional correctness. Several recent projects have demonstrated that formal, deductive functional-correctness verification is now possible for kernels, crypto, and compilers. Here I explain some of the modularity principles that make these verifications possible.
ISSN:2374-8303
DOI:10.1109/CSF.2016.8