It's time for trustworthy systems
Authors
NICTA
UNSW
Abstract
The time has arrived for truly trustworthy systems, backed by machine-checked proofs of security and reliability. Research demonstrates that formal whole-system analysis that applies to the C and binary implementation level is feasible, including proofs of integrity, authority confinement, confidentiality, and worst-case execution time. Because these proofs build on previous results, they become easier each year. However, they do have some limitations.
BibTeX Entry
@article{Heiser_MK_12, publisher = {IEEE Computer Society}, month = mar, journal = {IEEE Symposium on Security and Privacy}, paperurl = {https://ts.data61.csiro.au/publications/nicta_full_text/5778.pdf}, year = {2012}, keywords = {trustworthy systems, verification and analysis, sel4 microkernel, integrity, confidentiality, worst-case execution time, safety, security, computer security, functional correctness, authority confinement, noninterference}, volume = {10}, title = {It's Time for Trustworthy Systems}, number = {2}, author = {Heiser, Gernot and Murray, Toby and Klein, Gerwin}, pages = {67--70} }