Skip to content
/ different_traces Public

The Coq development for "Trace-Relating Compiler Correctness and Secure Compilation" paper

License

Apache-2.0 license
2 stars 0 forks Branches Tags Activity
Star
Notifications You must be signed in to change notification settings

secure-compilation/different_traces

BranchesTags

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

489 Commits
ResourceExhaustion
ResourceExhaustion
 
 
.gitignore
.gitignore
 
 
ANI.v
ANI.v
 
 
ChainModel.v
ChainModel.v
 
 
ClassicalExtras.v
ClassicalExtras.v
 
 
Composition.v
Composition.v
 
 
Def.v
Def.v
 
 
Galois.v
Galois.v
 
 
HSafetyCriterion.v
HSafetyCriterion.v
 
 
HSafetyPreservation.v
HSafetyPreservation.v
 
 
HyperCriterion.v
HyperCriterion.v
 
 
HyperDef.v
HyperDef.v
 
 
LICENSE
LICENSE
 
 
LanguageModel.v
LanguageModel.v
 
 
Makefile
Makefile
 
 
MoreTargetEventsExample.v
MoreTargetEventsExample.v
 
 
MyNotation.v
MyNotation.v
 
 
NoTrgGuarantees.v
NoTrgGuarantees.v
 
 
Properties.v
Properties.v
 
 
README.md
README.md
 
 
Relation4Correctness.v
Relation4Correctness.v
 
 
ResourceExhaustion.v
ResourceExhaustion.v
 
 
ResourceExhaustionExample.v
ResourceExhaustionExample.v
 
 
Robust2relHyperCriterion.v
Robust2relHyperCriterion.v
 
 
Robust2relHyperProperty.v
Robust2relHyperProperty.v
 
 
Robust2relSSCHCriterion.v
Robust2relSSCHCriterion.v
 
 
Robust2relSSCHPreservation.v
Robust2relSSCHPreservation.v
 
 
Robust2relSafetyCriterion.v
Robust2relSafetyCriterion.v
 
 
Robust2relSafetyProperty.v
Robust2relSafetyProperty.v
 
 
Robust2relTraceCriterion.v
Robust2relTraceCriterion.v
 
 
Robust2relTraceProperty.v
Robust2relTraceProperty.v
 
 
RobustHyperCriterion.v
RobustHyperCriterion.v
 
 
RobustHyperProperty.v
RobustHyperProperty.v
 
 
RobustHyperSafetyCriterion.v
RobustHyperSafetyCriterion.v
 
 
RobustHyperSafetyPreservation.v
RobustHyperSafetyPreservation.v
 
 
RobustSSCHCriterion.v
RobustSSCHCriterion.v
 
 
RobustSSCHPreservation.v
RobustSSCHPreservation.v
 
 
RobustSafetyCriterion.v
RobustSafetyCriterion.v
 
 
RobustSafetyPreservation.v
RobustSafetyPreservation.v
 
 
RobustTraceCriterion.v
RobustTraceCriterion.v
 
 
RobustTraceProperty.v
RobustTraceProperty.v
 
 
SSCHCriterion.v
SSCHCriterion.v
 
 
SSCHPreservation.v
SSCHPreservation.v
 
 
SafetyCriterion.v
SafetyCriterion.v
 
 
SafetyDef.v
SafetyDef.v
 
 
Stream.v
Stream.v
 
 
TraceCriterion.v
TraceCriterion.v
 
 
TraceModel.v
TraceModel.v
 
 
TypeRelationExample.v
TypeRelationExample.v
 
 
TypeRelationExampleInput.v
TypeRelationExampleInput.v
 
 
UcoPreservation.v
UcoPreservation.v
 
 
UcoRobustPreservation.v
UcoRobustPreservation.v
 
 
UndefBehavior.v
UndefBehavior.v
 
 
UndefBehaviorCompCert.v
UndefBehaviorCompCert.v
 
 
_CoqProject
_CoqProject
 
 

Repository files navigation

Trace-Relating Compiler Correctness and Secure Compilation

This repo contains the Coq development of the paper

Prerequisites for the Coq proofs

The Coq development is known to work with Coq v8.8.X and v8.9.X, and requires the following Coq library:

Replaying the Coq proofs

$ make -j4

License

This Coq development is licensed under the Apache License, Version 2.0 (see LICENSE) unless overridden by another license file.

About

The Coq development for "Trace-Relating Compiler Correctness and Secure Compilation" paper

Resources

Readme

License

Apache-2.0 license
Activity
Custom properties

Stars

2 stars

Watchers

3 watching

Forks

0 forks
Report repository

Releases

No releases published

Packages

No packages published

Contributors 5

Languages