Safe to the Last Instruction:Automated Verification of a Type-Safe Operating System
Jean Yang
Massachutts Institute of Technology Computer Science and Artificial Intelligence Laboratory Chris Hawblitzel Microsoft Rearch
Abstract
Typed asmbly language(TAL)and Hoare logic can verify the abnce of many kinds of errors in low-level code.We u TAL and Hoare logic to achieve highly automated,static verification of the safety of a new operating system called Verve.Our techniques and tools mechanically verify the safety of every asmbly language instruction in the operating system,run-time 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 rvices on top of the Nucleus,and applications that run on top of the kernel. The Nucleus,written in verified asmbly language,implements allocation,garbage collection,multiple stacks,interrupt handling, and device access.The kernel,written in C#and compiled to TAL, builds higher-level rvices,such as preemptive threads,on top of the Nucleus.A TAL checker verifies the safety of the kernel and applicat
ions.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,thefirst 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.
Categories and Subject Descriptors D.2.4[SOFTWARE ENGI-NEERING]:Software/Program Verification
General Terms Verification
Keywords Operating system,run-time system,verification,type safety
1.Introduction
High-level computer applications build on rvices provided by lower-level software layers,such as operating systems and lan-guage run-time systems.The lower-level software layers should be reliable and cure.Without reliability,urs endure frustration and potential data loss when the system software crashes.Without curity,urs are vulnerable to attacks from the network,which oft
en exploit low-level bugs such as buffer overflows to take over Permission to make digital or hard copies of all or part of this work for personal or classroom u is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on thefirst page.To copy otherwi,to republish,to post on rvers or to redistribute to lists,requires prior specific permission and/or a fee.
hit girl
avenuesPLDI’10,June5–10,2010,Toronto,Ontario,Canada.
Copyright c 2010ACM978-1-4503-0019/$10.00a ur’s computer.Unfortunately,today’s low-level software still suffers from a steady stream of bugs,often leaving computers vul-nerable to attack until the bugs are patched.
Many projects have propod using safe languages to increa the reliability and curity of low-level systems.Safe languages ensure type safety and memory safety:access to data are guar-anteed to be well-typed and guaranteed not to overflow memory boundaries or dereference dangling pointers.This safety rules out many common bugs,such as buffer overflow vulnerabilities.Un-fortunately,even if a language is safe,implementations of the lan-guage’s underlying run-time system might have bugs that under-mine the safety.For example,such bugs have left web browrs open to attack.
This paper prents Verve,an operating system and run-time system that we have verified to ensure type and memory safety. Verve has a simple mantra:every asmbly language instruction in the software stack must be mechanically verified for safety.This includes every instruction of every piece of software except the boot loader:applications,device drivers,thread scheduler,interrupt handler,allocator,garbage collector,etc.
The goal of formally verifying low-level OS and run-time sys-tem code is not new.Nevertheless,very little mechanically verified low-level OS and run-time system code exists,and that code still requires man-years of effort to verify[9,14].This paper argues that recent programming language and theorem-proving technolo-gies reduce this effort substantially,making it practical to verify strong properties throughout a complex system.The key idea is to split a traditional OS kernel into two layers:a critical low-level “Nucleus,”which exports esntial runtime abstractions of the un-derlying hardware and memory,and a higher-level kernel,which provides more fully-fledged rvices.Becau of the two dis-tinct layers,we can leverage two distinct automated technologies to verify Verve:TAL(typed asmbly language[18])and automated SMT(satisfiability modulo theories)theorem provers.Specifically, we verify the Nucleus using automated theorem proving(bad on Hoare Logic)and we ensure the safety of the kernel using TAL (generated from C#).Note that this two-layer
approach is not spe-cific to just Verve,but should apply more generally to systems that want to mix lower-level untyped code with higher-level typed code in a verifiably safe way.
撒娇英文
A complete Verve system consists of a Nucleus,a kernel,and one or more applications.We wrote the kernel and applications in safe C#,which is automatically compiled to TAL.An existing TAL checker[6]verifies this TAL(again,automatically).We wrote the Nucleus directly in asmbly language,hand-annotating it with asrtions(preconditions,postconditions,and loop invariants).An existing Hoare-style program verifier called Boogie[2]verifies the asmbly language against a specification of safety and correctness. This ensures the safety and correctness of the Nucleus’s implemen-
and safe in-
timer,key-
SMT the-
Writing the
Boogie
the Verve
executable
bad
system mechanically verified to ensure type safety.Furthermore,every asmbly language instruction that runs after booting is stat-ically verified(we do not have to trust a high-level-language compiler,nor do we have to trust any unverified library code).•It is a real system:it boots and runs on real,off-the-shelf x86 hardware,and supports realistic language features,including
class,virtual methods,arrays,and preemptive threads.
•It is efficient:it supports efficient TAL code generated by an op-timizing C#-to-TAL compiler,Bartok[6],using Bartok’s native layouts for objects,method tables,and arrays.It incorporates the code from earlier verified garbage collectors[13],which,as shown in[13],can run realistic macro-benchmarks at near the performance of Bartok’s native garbage collectors.
•It demonstrates that automated techniques(TAL and automated theorem proving)are powerful enough to verify the safety of the complex,low-level code that makes up an operating system and run-time system.Furthermore,it demonstrates that a small amount of code verified with automated theorem proving can support an arbitrary large amount of TAL code.
In its current implementation,Verve is a small system and has many limitations.It lacks support for many C#features:exception handling,for example,is implemented by killing a thread entirely, rather than with try/catch.It lacks the standard class library, since the library’s implementation currently contains much unsafe code.It lacks dynamic loading of code.It runs only on a single pro-cessor.Although it protects applications from each other using type safety,it lacks a more comprehensive isolation mechanism between applications,such as Java Isolates,C#AppDomains,or
Singularity SIPs[8].The verification does not guarantee termination.Finally, Verve us verified garbage collectors[13]that are stop-the-world rather than incremental or real-time,and Verve keeps interrupts dis-abled throughout the collection.
Except for multi-processor support,none of the limitations in Verve’s prent implementation are fundamental.We expect that with more time,the high degree of automation in Verve’s verifica-tion will allow Verve to scale to a more realistic feature t,such as a large library of safe code and a verified incremental garbage collector.
1.1Availability
All of the Verve source code is freely available for download or browsing at the following URL(brow the latest version under “Source Code”to e the“verify”directory,which contains Verve): /singularity
2.Tools for constructing a safe OS
Two complementary verification technologies,TAL and automated theorem proving,drive Verve’s design.On one hand,TAL is rela-tively easy to generate,since the compiler automatically turns C# co
de into TAL code,relying only on lightweight type annotations Figure1.Verve structure,showing all20functions exported by the Nucleus
already prent in the C#code.This enables TAL to scale easily to large amounts of code.For Verve,we u the Bartok compiler[6] to generate TAL code.
On the other hand,automated theorem provers can verify deeper logical properties about the code than a typical TAL type system can express.Leveraging this power requires more effort,though, in the form of heavyweight programmer-supplied preconditions, postconditions,and loop invariants.To exploit the tradeoff between TAL and automated theorem proving,we decided to split the Verve operating system code into two parts,shown in Figure1:a Nucleus, verified with automated theorem proving,and a kernel,verified with TAL.The difficulty of theorem proving motivated the balance between the two parts:only the functionality that TAL could not verify as safe went into the Nucleus;all other code went into the kernel.
The Nucleus’s source code is not expresd in TAL,but rather in Boogie’s programming language,called BoogiePL(or just Boo-gie),so that the Boogie verifier can check it.Since the Nucleus code consists of asmbly language instructions,the asmbly language instructions must appear
in a form that the Boogie verifier can understand.As described in detail below,we decided to encode asmbly language instructions as quences of calls to BoogiePL an“Add”procedure,a“Load”procedure,etc.),so that the Boogie verifier can check that each instruction’s precon-dition is satisfied.After Boogie verification,a parate tool called “BoogieAsm”,developed for an earlier project[13],extracts stan-dard asmbly language instructions from the BoogiePL code.A standard asmbler then turns the instructions into an objectfile.
Rather than hand-code all of the Nucleus in asmbly language, we wrote some of the less performance-critical parts in a high-level extension of BoogiePL that we call“Beat”.Our(non-optimizing) Beat compiler transforms verifiable Beat expressions and state-ments into verifiable BoogiePL asmbly language instructions.
In Figure2we show the trusted and untrusted components of our system.Besides the boot loader,the only trusted components are the tools ud to verify,asmble,and link the verified Nucleus and kernel.Note that none of our compilers are part of our trusted computing ba:we do not need to trust the compilers to ensure the correctness of the Nucleus and safety of the Verve system as a whole.As shown in Figure2,the TAL checker and Boogie/Z3 verifier check that the output of the compilers conforms to the TAL type system and the Nucleus specification,so we just need to trust th
e checkers.
Figure2.Building the Verve system:trusted,untrusted components Beyond the TAL checker and Boogie/Z3verifiers,Figure2 shows additional components in Verve’s trusted computing ba: the asmbler,the linker,the ISO CD-ROM image generator,and the boot loader.In addition,the trusted computing ba includes the specification of correctness for the Nucleus’s BoogiePL code.This includes specifications of the behavior of functions exported by the Nucleus,shown in Figure1.(For e
roger
xample,the specification of “YieldTo”ensures that the Nucleus ts the stack pointer to the top of the correct stack during a yield.)It also includes specifications for asmbly language instructions and for interaction with hard-ware devices and memory;we took some of the specifications from existing work[13],and wrote some of them from scratch.All Boogie specifications are written asfirst-order logic formulas in the BoogiePL language.
By expressing and checking properties at a low level(asm-bly language),we can ensure non-trivial properties with high con-fidence.The bulk of this paper focus on the properties,with an emphasis on the specification and verification of the Nucleus’s correctness properties.The next ction discuss the Nucleus’s de-sign,and subquent ctions discuss specification and verification.
3.The Nucleus interface
The core of our verification is the Nucleus,which provides a ver-ified interface to the low-level functionality of the operating sys-tem.We verify the Nucleus using Hoare logic in Boogie,bad on a trusted specification for x86asmbly language instructions.In Verve,all access to low-level functionality must occur through the Nucleus—the kernel’s TAL code and application’s TAL code can
only access low-level functionality indirectly,through the Nucleus. For example,TAL code cannot directly access device registers.Fur-thermore,even though TAL code can directly read and write words of memory,it can only read and write words designated as safe-for-TAL by the Nucleus’s garbage collector.
The Nucleus consists of a minimal t of functions necessary to support the TAL code that runs above it.We wanted a minimal t becau even with an automated theorem prover,Hoare-style verification is still hard work;less code in the Nucleus means less code to verify.At the same time,the t has to guarantee safety in the prence of arbitrary TAL code;it can assume that the TAL code is well typed,but can make no further assumptions about the behavior of the TAL code.For example,when an interrupt occurs,the Nucleus attempts to transfer control to a designated TAL interrupt handler.The Nucleus cannot assume that this handler is in the correct state to handle the interrupt,and must therefore check the handler’s state at run-time(e ction4.5).
One design decision greatly simplified the Nucleus:following a design ud in recent micro-kernels[11,14],no Nucleus function ever blocks.In other words,every Nucleus function performs a finite(and usually small)amount of work and then returns.The Nucleus may,however,return to a different thread than the thread that invoked the function.This allows the kernel built on top of the Nu
cleus to implement blocking thread operations,such as waiting on a maphore.
The design decisions led us to a small Nucleus API consist-ing of just20functions,all shown in Figure1.The20func-tions,implemented with a total of about1500x86instructions,in-clude3memory management functions(AllocObject,AllocVec-tor,GarbageCollect),one very limited exception handling func-tion(Throw),3stack management functions(GetStackState,Re-tStack,YieldTo),and4device access functions(VgaTextWrite, TryReadKeyboard,StartTimer,SendEoi).Most of the functions are intended for u only by the kernel,not by applications.However, applications may call AllocObject and AllocVector directly.
The Nucleus exports four pudo-functions,readField,write-Field,readStack,and writeStack,to the kernel and applications. The functions,described further in ction4,contain no exe-cutable code,but their verification guarantees that the kernel and applications willfind the values that they expect when they try to accessfields or objects or slots on the current stack.The Nucleus exports another4functions to the hardware for handling faults and interrupts:FatalHandler halts the system,while FaultHandler,Er-rorHandler,and InterruptHandler yield execution to kernel TAL code running on a designated interrupt-handling stack.Finally,the Nucleus exports an entry point,NucleusEntryPoint to the boot loader.
As more devices are added to the system,more Nucleus func-tions may be required.However,a minimal Nucleus only needs to include the portion of the device interfaces critical the rest of the system’s safety;if desired,Verve could u an I/O MMU to protect the system from devices,minimizing the device code that needs to reside in the Nucleus.
Following the approach taken by the recent verified L4micro-kernel,L4[14],Verve keeps interrupts disabled throughout the execution of any single Nucleus function.(On the other hand,in-terrupts may be enabled during the TAL kernel’s execution,with no loss of safety.)Since Nucleus functions do not block,Verve still guarantees that eventually,interrupts will always be re-enabled,and usually will be re-enabled very quickly.However,Verve’s current implementation sacrifices real-time interrupt handling becau of one particularly long function:“GarbageCollect”,which performs an entire stop-the-world garbage collection.This is currently a sub-stantial limitation for the responsiveness of the system,but it is not fundamental to Verve’s approach.Given a verified incremental col-lector,Verve could reduce the execution time of“GarbageCollect”to,say,just the time required to scan the stacks(or even a single stack),rather than the time required to garbage collect the whole heap.(Alternatively,Verve could poll for interrupts periodically, as in L4.However,delivering the interrupts to the kernel TAL code would still require that the garbage collector reach a state that is safe for the kernel.)
The next two ctions describes how Verve specifies,imple-ments,and verifies the Nucleus functions listed above.
4.The Nucleus specification
To verify that the Nucleus behaves correctly,we have to spec-ify what correct behavior is.Formally,this specification con-
sists of preconditions and postconditions for each of the20func-tions exported by the Nucleus(Figure1).The preconditions reflect the guarantees made by other components of the sys-tem when calling the Nucleus.For example,the precondition to NucleusEntryPoint describes the state of memory when the Nu-cleus begins execution;the(trusted)boot loader is responsible for establishing this precondition.The preconditions for functions ex-ported to the kernel and applications describe the state of regis-ters and the current stack when making a call to the Nucleus;the (trusted)TAL checker is responsible for guaranteeing that the preconditions hold when the(untrusted)kernel and applications transfer control to the Nucleus.(Note that any property not guar-anteed by the TAL checker cannot be assumed by the Nucleus’s preconditions for functions exported to the kernel and applications; as a result,the Nucleus must occasionally perform run-time c
hecks to validate the values pasd from the kernel and applications.) When writing the Nucleus’s specification,we are not interested so much in the Nucleus’s private,internal behaviors,but rather how the Nucleus interacts with other components of the system. For example,the Verve specification of garbage collection does not specify which algorithm the garbage collector should pying or mark-sweep),since the algorithm is an in-ternal behavior that is irrelevant to the other components of the system.Instead,following the approach of McCreight et al[17], the specification simply says that the garbage collector must main-tain the well-formedness of the stacks and heap,so that subquent reads and writes to the stack and heap other components of the sys-tem behave as expected.(Internally,the garbage collectors ud by Verve[13]do have stronger invariants about specific details of the algorithm,but the invariants are kept hidden from the other Verve system components.)
The Nucleus interacts withfive components:memory,hard-ware devices,the boot loader,interrupt handling,and TAL code (kernel and application code).Memory and hardware devices ex-port functionality to the Nucleus,such as the ability to read mem-ory locations and write hardware registers.Verve must verify that the Nucleus satisfies the preconditions to each operation on mem-ory and hardware.In turn,the Nucleus exports functionality to the boot loader(the Nucleus entry point),
the interrupt handling (the Nucleus’s interrupt handlers),and the TAL code(AllocObject, YieldTo,etc.).
愚人笑话4.1Specification logistics
Verve express the specification for interacting with the compo-nents asfirst-order logical formulas in BoogiePL[2].The formu-las follow C/Java/C#syntax and consist of:
•arithmetic operators:+,-,*,>,==,!=,...
•boolean operators:!,&&,||,==>,...
•variables:foo,Bar,old(foo),...
•boolean constants:true,fal
•integer constants:5,...
•bit vector contants:5bv16,5bv32,...
•function application:Factorial(5),Max(3,7),IsOdd(9),...•array indexing:foo[3],...
•array update:foo[3:=Bar],...
英语新闻评论•quantified formulas:(∀i:int::foo[i]==Factorial(i)),... For a variable foo,the expression old(foo)refers to the value of foo at the beginning of the procedure.BoogieAsm also enforces the convention that capitalized variable names correspond with read-only variables.For instance,the variable corresponding to the instruction pointer Eip is read-only,while variable corresponding to the register eax is directly readable and writable.
BoogiePL bit vectors correspond to integers in C/Java/C#, which are limited to numbers thatfit inside afixed number of bits. BoogiePL integers,on the other hand,are unbounded mathemati-cal integers.BoogiePL arrays are unbounded mathematical maps from some type(usually integers)to some other type.Unlike ar-rays in C/Java/C#,BoogiePL arrays are immutable values(there are no references to arrays and arrays are not updated in place). An array update expression a[x:=y]creates a new array,which is equal to the old array a at all locations except x,where it con-tains a new value,y.For example,(a[x:=y])[x]==y and (a[x:=y])[x+1]==a[x+1]).
BoogiePL procedures have preconditions and postconditions, written as BoogiePL logical formulas:
var a:int,b:int;
procedure P(x:int,y:int)
requires a<b&&x<y;
modifies a,b;
sanitationensures a<b&&a==x+old(a);
{
a:=a+x;
b:=b+y;
}
In this example,the procedure P can only be called in a state where global variable a is less than global variable b,and the parameter x is less than the parameter y.Upon exit,the procedure’s postconditions ensure that a is still less than b,and that a is equal to x plus the old version of a(before P executed).Note that the procedure must explicitly reveal all the global variables that it modifies(“modifies a,b;”in this example),so that callers to the procedure will be aware of the modifications.
heheheiTo verify that a program’s code obeys its specification,the Boo-gie tool relies on the Z3[7]automated theorem prover.Z3automat-ically checks logical formulas involving linear arithmetic(addition, subtraction,comparison),arrays,bit vectors,and functions.Z3also checks quantified formulas(formulas with forall and exists); however,Z3relies on programmer-supplied hints in the form of triggers to help with quantifiers,since checking quantified formu-las with arithmetic and arrays is undecidable in general.Earlier work[13]describes how Verve’s garbage collectors u triggers.
For each function exported to the boot loader,interrupt han-dling,and TAL code,the Nucleus implements a BoogiePL proce-dure who specification is given in terms of“requires”,“ensures”, and“modifies”claus.The Nucleus implements the procedures in terms of more primitive hardware procedures:each BoogiePL procedure exported from the memory and hardware devices to the Nucleus corresponds to exactly one asmbly language instruction, such as an instruction to read a single memory location or write to a single hardware register.
In order to convey concretely what the Nucleus specification and verification entail,subctions4.2-4.6describe in detail the BoogiePL specifications of the Nucleus’s interaction with the mem-ory(4.2),hardware devices(4.3),boot loader(4.4),interrupt han-dling(4.5),and TAL code(4.6).Note that the interfaces in sub-ctions4.2-4.5are for u only by the Nucleus,not by kernel and application co
de.Kernel and application code can only make u of the interfaces indirectly,via calls to the Nucleus.
4.2Memory
Verve’s initial memory layout is t by the boot loader.Verve us the boot loader from the Singularity project[8],which ts up an initial virtual-memory address it ts up a page table), loads the executable image into memory,and jumps to the exe-cutable’s entry point,passing detailed information about the mem-
ory layout to the entry point.The boot-loader-supplied address space simply maps virtual memory directly to physical memory, except for a small range of low address that are left unmapped (to catch null pointer dereferences).A traditional operating system would create new virtual memory address spaces to protect appli-cations from each other.However,unlike traditional operating sys-tems,Verve guarantees type safety,and can therefore rely on type safety for protection.Becau of this,Verve simply keeps the initial boot-loader-supplied address space.
Verve’s mapped address space consists of three parts.First is the memory occupied by the executable image,including code, staticfields,method tables,and memory layout information for the g
arbage collector.Verve may read this memory,but may write only to the staticfields,not the code,method tables,or layout infor-mation.Second,the Verve specification rerves the memory just above the executable image for the interrupt table.Verve may write to the table,but it can only write values that obey the specification for interrupt handlers.Third,the remaining memory above the in-terrupt handler is general-purpo memory,free for arbitrary u; the Nucleus may read and write it at any time as it wishes(as long as it ensures the well-formedness of the heap and current stack be-fore transferring control to TAL code,as discusd in ction4.6).
The specification describes the state of general-purpo memory using a global variable Mem,which is an array that maps integer byte address to integer values.For any4-byte-aligned address i in general-purpo memory,Mem[i]contains the32-bit memory contents stored at address i,reprented as an integer in the 232−1.The memory exports two operations to the Nucleus, Load and Store:
procedure Load(ptr:int)returns(val:int);
requires memAddr(ptr);
requires Aligned(ptr);
modifies Eip;
ensures word(val);
ensures val==Mem[ptr];
procedure Store(ptr:int,val:int);
requires memAddr(ptr);
requires Aligned(ptr);
requires word(val);
modifies Eip,Mem;
ensures Mem==old(Mem)[ptr:=val];
Each of the two operations requires a4-byte-aligned pointer (“Aligned(...)”)to memory inside the general-purpo memory region(“memAddr(...)”).The loaded or stored value must be in 232−1(“word(...)”).Any Store operation updates the contents of Mem,so that subquent Lo
ad operations are guaranteed to e the updated value.Loads and stores have an additional side effect,noted in the modifies clau:they modify the current instruction pointer(program counter),“Eip”.
The executable image memory exports its own load/store inter-face to the Nucleus,but with a store operation that applies only to staticfields.
Finally,the interrupt table exports a store operation that allows the Nucleus to write to the interrupt descriptor table(IDT).On x86 processors,the interrupt descriptor table contains a quence of8-byte entries that describe what code the processor should jump to when receiving various kinds of faults and interrupts.This is a very nsitive data structure,since an invalid entry could cau a jump to an arbitrary address in memory,which would be unsafe.We had originally hoped to u general-purpo memory for the interrupt table,and to guarantee the well-formedness of the interrupt table whenever the Nucleus transfers control to TAL code.Under this hope,the Nucleus would be allowed to arbitrarily modify the in-terrupt table temporarily,which would be safe while interrupts are disabled.However,some x86platforms support“non-maskable in-terrupts”,which can occur even with interrupts disabled.If such an interrupt ever occurred,we’d feel safer transferring control to
a designated fatal error handler than allowing arbitrary behavior. Therefore,the interrupt table exports an interface that only allows stores of approved entries:
procedure IdtStore(entry:int,offt:int,wipedata
handler:int,ptr:int,val:int); requires0<=entry&&entry<256;
requires(offt==0&&val==IdtWord0(handler)) ||(offt==4&&val==IdtWord4(handler)); requires IsHandlerForEntry(entry,handler); requires ptr==idtLo+8*entry+offt; modifies Eip,IdtMem,IdtMemOk;
ensures IdtMem==old(IdtMem)[ptr:=val];
ensures IdtMemOk==old(IdtMemOk)[ptr:=true];
Like Store,IdtStore corresponds to a single x86store in-struction.Using IdtStore,the Nucleus may write to either4-byte word of any8-byte entry in the table,as long as the word describes
a valid interrupt handler for the entry.After a valid word is writ-ten to address ptr,the specification updates an array of booleans “IdtMemOk”to reflect that the word at address ptr is now valid. Valid words obey a strange Intel specification that splits the han-dler’s address across the two words in16-bit pieces;we show the BoogiePL for this specification just to demonstrate that Verve can deal with such low-level architectural details safely(and,or,and shl are32-bit bitwi AND/OR/SHIFT-LEFT):
北京新东方雅思培训
function IdtWord0(handler:int)returns(int){
or(shl(CSS,16),and(handler,0x0000ffff))
}
function IdtWord4(handler:int)returns(int){
or(and(handler,0xffff0000),0x8e00)
}
4.3Hardware devices
Verve currently supports four hardware devices:a programmable interrupt controller(PIC),a programmable interval timer(PIT),a VGA text screen,and a keyboard.Verve specifies the interaction with this hardware using unbounded streams of events.The Nu-cleus delivers events to the PIC,PIT,and screen,and it receives events from the keyboard.For the screen,the events are commands
to draw a character at a particular position on the screen.For the keyboard,events are keystrokes received from the keyboard.For the PIC and PIT,particular quences of events initialize interrupt handling and start timers.
We prent the keyboard specification as an example.Verve reprents the stream of events from the keyboard as an immutable array KbdEvents mapping event quence numbers(reprented as integers,starting from0)to events(also reprented as integers). As the Nucleus queries the keyboard,it discovers more and more events from the stream.Two indices into the array,KbdAvailable and KbdDone,indicate the state of the Nucleus’s interaction with the KbdDone-1have already been read by the Nucleus,while KbdAvailable-1are available
to read but have not yet been read.
Two operations,KbdStatusIn8and KbdDataIn8,query the keyboard.Each of the procedures reprents a single8-bit x86 asmbly language I/O instruction,and BoogieAsm translates each call to the procedures into a single x86“in”instruction.By invoking KbdStatusIn8,the Nucleus discovers the current state of
