Demo Data from VLDB 2026 / reviewers in the wild / expert
Guglielmo Fachini
dblp:204/9454
· DBLP profile ↗
2ranked-venue papers
1as first author
0since 2021 · last 2018
—ORCID · none
Domains — the database's venue-derived domains; a paper can count in several
Security and privacy · 1Software engineering, systems software and programming languages · 1 · 1 first-author
Expertise — from the expertise taxonomy: the topics of the expert's papers under the CCF categories. A weight counts papers with recency: 1 for a paper about the topic, 0.3 when the topic is its context, halved every five years.
| Network and information security
1 paper |
Systems and software security · 100% | |
| Software engineering, system software, and programming languages
1 paper |
Programming languages and type systems · 100% |
Topics — the 4 heaviest of 4, each with the papers that count most for it
| Topic | Weight | Papers | Last | Evidence papers |
|---|---|---|---|---|
Systems and software security › language-based security
secure compilation |
0.3 | 1 | 2018 | When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise · CCS 2018 |
Programming languages and type systems
language semantics |
0.3 | 1 | 2018 | When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise · CCS 2018 |
Systems and software security › isolation
compartmentalization |
0.1 | 1 | 2018 | When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise · CCS 2018 |
Systems and software security › isolation
software fault isolation |
0.1 | 1 | 2018 | When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise · CCS 2018 |
Methods — techniques the papers use, named apart from their topics
tag-based reference monitor · 0.7coq proofs · 0.3coq proof · 0.3
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2018 | When Good Components Go Bad: Formally Secure Compilation Despite Dynamic CompromiseabstractWe propose a new formal criterion for evaluating secure compilation schemes for unsafe languages, expressing end-to-end security guarantees for software components that may become compromised after encountering undefined behavior---for example, by accessing an array out of bounds. Our criterion is the first to model dynamic compromise in a system of mutually distrustful components with clearly specified privileges. It articulates how each component should be protected from all the others---in particular, from components that have encountered undefined behavior and become compromised. Each component receives secure compilation guarantees---in particular, its internal invariants are protected from compromised components---up to the point when this component itself becomes compromised, after which we assume an attacker can take complete control and use this component's privileges to attack other components. More precisely, a secure compilation chain must ensure that a dynamically compromised component cannot break the safety properties of the system at the target level any more than an arbitrary attacker-controlled component (with the same interface and privileges, but without undefined behaviors) already could at the source level. To illustrate the model, we construct a secure compilation chain for a small unsafe language with buffers, procedures, and components, targeting a simple abstract machine with built-in compartmentalization. We give a careful proof (mostly machine-checked in Coq) that this compiler satisfies our secure compilation criterion. Finally, we show that the protection guarantees offered by the compartmentalized abstract machine can be achieved at the machine-code level using either software fault isolation or a tag-based reference monitor. Carmine Abate, Arthur Azevedo de Amorim, Roberto Blanco, Ana Nora Evans, Guglielmo Fachini, Catalin Hritcu, Théo Laurent, Benjamin C. Pierce, Marco Stronati, Andrew P. Tolmach |
CCS | 5 |
| 2017 | Validating the Meta-Theory of Programming Languages (Short Paper)
Guglielmo Fachini, Alberto Momigliano |
SEFM | 1 |