NDLI: Safety checking of machine code

Please wait, while we are loading the content...

Dynamo: a transparent dynamic optimization system

Practicing JUDO: Java under dynamic optimizations

Split-stream dictionary program compression

Unification-based pointer analysis with directional assignments

Off-line variable substitution for scaling points-to analysis

Modular interprocedural pointer analysis using access paths: design, implementation, and evaluation

Safety checking of machine code

Translation validation for an optimizing compiler

A certifying compiler for Java

Bidwidth analysis with application to silicon compilation

Optimal instruction scheduling using integer programming

Improved spill code generation for software pipelined loops

Exploiting superword level parallelism with multimedia instruction sets

Compiler analysis of irregular memory accesses

Transforming loops to recursion for multi-level memory hierarchies

Symbolic bounds analysis of pointers, array indices, and accessed memory regions

A framework for interprocedural optimization in the presence of dynamic class loading

Effective synchronization removal for Java

Type-based race detection for Java

On loops, dominators, and dominance frontier

Functional reactive programming from first principles

Scalable context-sensitive flow analysis using instantiation constraints

Contaminated garbage collection

A generational on-the-fly garbage collector for Java

A single intermediate language that supports multiple implementations of exceptions

Efficient algorithms for bidirectional debugging

Caching function calls using precise dependencies

ABCD: eliminating array bounds checks on demand

Field analysis: getting useful and low-cost interprocedural information

An automatic object inlining optimization and its evaluation

Safety checking of machine code

Content Provider	ACM Digital Library
Author	Miller, Barton P. Reps, Thomas Xu, Zhichen
Abstract	We show how to determine statically whether it is safe for untrusted machine code to be loaded into a trusted host system.Our safety-checking technique operates directly on the untrusted machine-code program, requiring only that the initial inputs to the untrusted program be annotated with typestate information and linear constraints. This approach opens up the possibility of being able to certify code produced by any compiler from any source language, which gives the code producers more freedom in choosing the language in which they write their programs. It eliminates the dependence of safety on the correctness of the compiler because the final product of the compiler is checked. It leads to the decoupling of the safety policy from the language in which the untrusted code is written, and consequently, makes it possible for safety checking to be performed with respect to an extensible set of safety properties that are specified on the host side.We have implemented a prototype safety checker for SPARC machine-language programs, and applied the safety checker to several examples. The safety checker was able to either prove that an example met the necessary safety conditions, or identify the places where the safety conditions were violated. The checking times ranged from less than a second to 14 seconds on an UltraSPARC machine.
Starting Page	70
Ending Page	82
Page Count	13
File Format	PDF
ISBN	1581131992
DOI	10.1145/349299.349313
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2000-08-01
Publisher Place	New York
Access Restriction	Subscribed
Content Type	Text
Resource Type	Article

Central Library (ISO-9001:2015 Certified)
Indian Institute of Technology Kharagpur
Kharagpur, West Bengal, India | PIN - 721302

See location in the Map
03222 282435
Mail: support@ndl.gov.in

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in