Ticket #1698 (new cage)

Opened 4 years ago

Investigate SAFECode

Reported by: petdance Owned by:
Priority: normal Milestone:
Component: none Version: 2.5.0
Severity: medium Keywords:
Cc: Language:
Patch status: Platform:

Description

 http://safecode.cs.illinois.edu/

The purpose of the SAFECode project is to enable program safety without garbage collection and with minimal run-time checks using static analysis when possible and run-time checks when necessary. SAFECode defines a code representation with minimal semantic restrictions designed to enable static enforcement of safety, using aggressive compiler techniques developed in this project.

SAFECode is designed to provide the following safety guarantees:

  • Array bounds checking (prevents pointers from overflowing from one memory object into another)
  • Loads and stores only access valid memory objects
  • Type safety for a subset of memory objects proven to be type-safe
  • Sound operational semantics in the face of dangling pointer errors (i.e., all safety guarantees hold even when dangling pointers are dereferenced).
  • Optional dangling pointer detection (induces more overhead)
Note: See TracTickets for help on using tickets.