Skip to content

Simple kernel-level programs to be verified using the ACL2-based x86isa reasoning framework

Notifications You must be signed in to change notification settings

shigoel/Ring0Code

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

6 Commits
 
 
 
 
 
 

Repository files navigation

Ring0Code
Author: Shilpi Goel <shigoel@gmail.com>

----------------------------------------------------------------------

This repository contains some very simple kernel sub-routines/programs
that will be used to exercise the ACL2-based x86isa reasoning
framework (see books/projects/x86isa on https://github.com/acl2/acl2).

By design, these system programs are much simpler (and less efficient,
less complete, etc.) than the in-use kernel code. Using these programs
as verification targets in the "System-level Mode" of the x86isa
framework will give an idea of what to expect when verifying in-use
kernel code later.

If you choose to compile and execute the programs in this repository,
please do so on a Linux distribution on a virtual machine. These
programs could mess up your system (they contain privileged code after
all and are written for experimentation purposes). And oh, I don't
take any responsibility if bad things happen to your machine after you
use these programs.

----------------------------------------------------------------------

About

Simple kernel-level programs to be verified using the ACL2-based x86isa reasoning framework

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published