Results 1-20 of 29.
((uid:50009167))

Bookmark and Share    
Peer Reviewed
See detailBar Induction: The Good, the Bad, and the Ugly
Rahli, Vincent UL; Bickford, Mark; Constable, Robert

in Abstract book of LICS 2017: 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (2017)

Detailed reference viewed: 44 (9 UL)
Full Text
Peer Reviewed
See detailFormally Verified Differential Dynamic Logic
Bohrer, Brandon; Rahli, Vincent UL; Vukotic, Ivana UL et al

in CPP 2017 (2017)

Detailed reference viewed: 101 (21 UL)
Full Text
Peer Reviewed
See detailAvoiding Leakage and Synchronization Attacks through Enclave-Side Preemption Control
Volp, Marcus UL; Lackorzynski, Adam; Decouchant, Jérémie UL et al

Scientific Conference (2016, December 12)

Intel SGX is the latest processor architecture promising secure code execution despite large, complex and hence potentially vulnerable legacy operating systems (OSs). However, two recent works identified ... [more ▼]

Intel SGX is the latest processor architecture promising secure code execution despite large, complex and hence potentially vulnerable legacy operating systems (OSs). However, two recent works identified vulnerabilities that allow an untrusted management OS to extract secret information from Intel SGX's enclaves, and to violate their integrity by exploiting concurrency bugs. In this work, we re-investigate delayed preemption (DP) in the context of Intel SGX. DP is a mechanism originally proposed for L4-family microkernels as disable-interrupt replacement. Recapitulating earlier results on language-based information-flow security, we illustrate the construction of leakage-free code for enclaves. However, as long as adversaries have fine-grained control over preemption timing, these solutions are impractical from a performance/complexity perspective. To overcome this, we resort to delayed preemption, and sketch a software implementation for hypervisors providing enclaves as well as a hardware extension for systems like SGX. Finally, we illustrate how static analyses for SGX may be extended to check confidentiality of preemption-delaying programs. [less ▲]

Detailed reference viewed: 146 (21 UL)
Full Text
See detailExercising Nuprl's Open-Endedness
Rahli, Vincent UL

in The 5th International Congress on Mathematical Software (2016)

Detailed reference viewed: 52 (8 UL)
Full Text
Peer Reviewed
See detailA Nominal Exploration of Intuitionism
Rahli, Vincent UL; Bickford, Mark

in The 5th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2016) (2016)

Detailed reference viewed: 56 (12 UL)
Full Text
Peer Reviewed
See detailSkalpel: A Constraint-Based Type Error Slicer for Standard ML
Rahli, Vincent UL; Wells, Joe; Pirie, John et al

in Journal of Symbolic Computation (2016)

Detailed reference viewed: 57 (9 UL)
Full Text
Peer Reviewed
See detailCoq as a Metatheory for Nuprl with Bar Induction
Rahli, Vincent UL; Bickford, Mark

Scientific Conference (2015)

Detailed reference viewed: 33 (13 UL)
Full Text
Peer Reviewed
See detailFormal Specification, Verification, and Implementation of Fault-Tolerant Systems using EventML
Rahli, Vincent UL; Guaspari, David; Bickford, Mark et al

in EASST (2015)

Detailed reference viewed: 38 (5 UL)
Full Text
Peer Reviewed
See detailSkalpel: A Type Error Slicer for Standard ML
Rahli, Vincent UL; Wells, Joe B.; Pirie, John et al

in Electronic Notes in Theoretical Computer Science (2015)

Detailed reference viewed: 25 (1 UL)
Full Text
Peer Reviewed
See detailTowards a Formally Verified Proof Assistant
Anand, Abhishek; Rahli, Vincent UL

in Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings (2014)

Detailed reference viewed: 27 (5 UL)
Full Text
See detailTowards a Formally Verified Proof Assistant (technical report)
Anand, Abhishek; Rahli, Vincent UL

Report (2014)

Detailed reference viewed: 22 (2 UL)
Full Text
Peer Reviewed
See detailA Generic Approach to Proofs about Substitution
Anand, Abhishek; Rahli, Vincent UL

in LFMTP 2014 (2014)

Detailed reference viewed: 24 (2 UL)
Full Text
Peer Reviewed
See detailA Type Theory with Partial Equivalence Relations as Types
Anand, Abhishek; Bickford, Mark; Constable, Robert L. et al

Scientific Conference (2014)

Detailed reference viewed: 19 (5 UL)
Full Text
Peer Reviewed
See detailDeveloping Correctly Replicated Databases Using Formal Tools
Schiper, Nicolas; Rahli, Vincent UL; Van Renesse, Robbert et al

in DSN 2014 (2014)

Detailed reference viewed: 14 (5 UL)
Full Text
Peer Reviewed
See detailFormal Program Optimization in Nuprl Using Computational Equivalence and Partial Types
Rahli, Vincent UL; Bickford, Mark; Anand, Abhishek

in ITP 2013 (2013)

Detailed reference viewed: 10 (1 UL)
Full Text
Peer Reviewed
See detailReducibility proofs in the lambda-calculus
Kamareddine, Fairouz; Rahli, Vincent UL; Wells, J. B.

in Fundamenta Informaticae (2012), 121

Detailed reference viewed: 12 (0 UL)
Full Text
Peer Reviewed
See detailLogic of Events, a framework to reason about distributed systems
Bickford, Mark; Constable, Robert L.; Rahli, Vincent UL

Scientific Conference (2012)

Detailed reference viewed: 13 (1 UL)
Full Text
Peer Reviewed
See detailOn Realisability Semantics for Intersection Types with Expansion Variables.
Kamareddine, Fairouz; Nour, Karim; Rahli, Vincent UL et al

in Fundamenta Informaticae (2012), 121

Detailed reference viewed: 10 (0 UL)
Full Text
See detailIntroduction to EventML
Bickford, Mark; Constable, Robert L.; Eaton, Richard et al

Report (2012)

Detailed reference viewed: 19 (1 UL)