Safe to the last instruction.
Typed assembly language (TAL) and Hoare logic can be used to verify the absence of many kinds of errors in low-level code. We use TAL and Hoare logic to achieve highly automated, static verification of the safety of a new operating system called Verve. We have developed techniques and tools to mecha...
| Publicado en: | Communications of the ACM Vol. 54; no. 12; pp. 123 - 132 |
|---|---|
| Autores principales: | , |
| Formato: | Artículo |
| Publicado: |
Association for Computing Machinery
Dec2011
|
| Materias: | |
| Acceso en línea: | Ver este registro en EBSCOhost |
| fields | @attributes: recordID: 1 pdfLink: plink: https://search.ebscohost.com/login.aspx?direct=true&db=hlh&AN=69924584&site=ehost-live header: @attributes: shortDbName: hlh uiTerm: 69924584 longDbName: Humanities International Complete uiTag: AN controlInfo: bkinfo: jinfo: jid: 00010782 ACM jtl: Communications of the ACM issn: 00010782 maglogo: N pubinfo: dt: Dec2011 vid: 54 iid: 12 pid: 68 pub: Association for Computing Machinery artinfo: ui: 69924584 10.1145/2043174.2043197 ppf: 123 ppct: 9 formats: tig: atl: Safe to the last instruction. aug: au: Yang, Jean Hawblitzel, Chris su: Assembly languages (Electronic computers) Hoare logic Computer programming Computer operating systems C# (Computer program language) Debugging sug: subj: Assembly languages (Electronic computers) Hoare logic Computer programming Computer operating systems C# (Computer program language) Debugging ab: Typed assembly language (TAL) and Hoare logic can be used to verify the absence of many kinds of errors in low-level code. We use TAL and Hoare logic to achieve highly automated, static verification of the safety of a new operating system called Verve. We have developed techniques and tools to mechanically verify the safety of every assembly-language instruction in the operating system, runtime system, drivers, and applications (in fact, every part of the system software except the boot loader). Verve consists of a Nucleus that provides primitive access to hardware and memory, a kernel that builds services on top of the Nucleus, and applications that run on top of the kernel. The Nucleus, written in verified assembly language, implements allocation, garbage collection, multiple stacks, interrupt handling, and device access. The kernel, written in C# and compiled to TAL, builds higher-level services, such as preemptive threads, on top of the Nucleus. A TAL checker verifies the safety of the kernel and applications. A Hoare-style verifier with an automated theorem prover verifies both the safety and correctness of the Nucleus. Verve is, to the best of our knowledge, the first operating system mechanically verified to guarantee both type and memory safety. More generally, Verve s approach demonstrates a practical way to mix high-level typed code with low-level untyped code in a verifiably safe manner. pubtype: Periodical doctype: Article src: R language: English refInfo: copyright: @attributes: flag: Y dt: @attributes: year: 2011 holdings: @attributes: islocal: N |
|---|