4 papers
SECOMP: Formally Secure Compilation of Compartmentalized C Programs
Jérémy Thibault, Roberto Blanco, Dongjae Lee +5
Undefined behavior in C often causes devastating security vulnerabilities. One practical mitigation is compartmentalization, which allows developers to structure large programs int…
Pathfinding Future PIM Architectures by Demystifying a Commercial PIM Technology
Bongjoon Hyun, Taehun Kim, Dongjae Lee +1
Processing-in-memory (PIM) has been explored for decades by computer architects, yet it has never seen the light of day in real-world products due to their high design overheads an…
Conditional Contextual Refinement (CCR)
Youngju Song, Minki Cho, Dongjae Lee +1
Contextual refinement (CR) is one of the standard notions of specifying open programs. CR has two main advantages: (i) (horizontal and vertical) compositionality that allows us to…
Abstraction Logic: The Marriage of Contextual Refinement and Separation Logic
Youngju Song, Minki Cho, Dongjae Lee +1
Contextual refinement and separation logics are successful verification techniques that are very different in nature. First, the former guarantees behavioral refinement between a c…