Demonstration venue · read-only. Every page can be browsed; the buttons that would change it are switched off. Create an account to run TaxoReview on your own data. A simulation from public publication records: the people listed were not invited and did not agree to review.
? Tutorial for this page

David A. Ramos

dblp:32/1943 · DBLP profile ↗
← Back
4ranked-venue papers
3as first author
0since 2021 · last 2016
—ORCID · none

Domains — the database's venue-derived domains; a paper can count in several

Systems, architecture and hardware · 2 · 1 first-authorSecurity and privacy · 1 · 1 first-authorSoftware engineering, systems software and programming languages · 1 · 1 first-authorTheory of computation · 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.

Software engineering, system software, and programming languages
4 papers
Program analysis · 86% Program verification · 11% Compilers and program optimization · 3%
Network and information security
1 paper
Blockchain and cryptocurrency security · 100%
Computer architecture, parallel and distributed computing, and storage systems
1 paper
Processor architecture and microarchitecture · 100%

Topics — the 5 heaviest of 7, each with the papers that count most for it

TopicWeightPapersLastEvidence papers
Program analysis
symbolic execution
0.522016
Under-Constrained Symbolic Execution: Correctness Checking for Real Code · USENIX ATC 2016
Under-Constrained Symbolic Execution: Correctness Checking for Real Code · USENIX Security Symposium 2015
Program analysis › symbolic execution
under-constrained symbolic execution
0.522016
Under-Constrained Symbolic Execution: Correctness Checking for Real Code · USENIX ATC 2016
Under-Constrained Symbolic Execution: Correctness Checking for Real Code · USENIX Security Symposium 2015
Program verification
equivalence checking
0.112011
Practical, Low-Effort Equivalence Verification of Real Code · CAV 2011
Blockchain and cryptocurrency security › smart contract security
vulnerability detection
0.112008
Testudo: Heavyweight security analysis via statistical sampling · MICRO 2008
Compilers and program optimization
compiler correctness
0.012011
Practical, Low-Effort Equivalence Verification of Real Code · CAV 2011

Methods — techniques the papers use, named apart from their topics

symbolic execution · 0.3tagged memory · 0.2statistical sampling · 0.2distributed debugging · 0.2equivalence checking · 0.1
YearPublicationVenuePosition
2016 Under-Constrained Symbolic Execution: Correctness Checking for Real Code
David A. Ramos, Dawson R. Engler
USENIX ATC1
2015 Under-Constrained Symbolic Execution: Correctness Checking for Real Code
David A. Ramos, Dawson R. Engler
USENIX Security Symposium1
2011 Practical, Low-Effort Equivalence Verification of Real Code
David A. Ramos, Dawson R. Engler
CAV1
2008 Testudo: Heavyweight security analysis via statistical sampling
abstract
Heavyweight security analysis systems, such as taint analysis and dynamic type checking, are powerful technologies used to detect security vulnerabilities and software bugs. Traditional software implementations of these systems have high instrumentation overhead and suffer from significant performance impacts. To mitigate these slowdowns, a few hardware-assisted techniques have been recently proposed. However, these solutions incur a large memory overhead and require hardware platform support in the form of tagged memory systems and extended bus designs. Due to these costs and limitations, the deployment of heavyweight security analysis solutions is, as of today, limited to the research lab. In this paper, we describe Testudo, a novel hardware approach to heavyweight security analysis that is based on statistical sampling of a programpsilas dataflow. Our dynamic distributed debugging reduces the memory overhead to a small storage space by selectively sampling only a few tagged variables to analyze during any particular execution of the program. Our system requires only small hardware modifications: it adds a small sample cache to the main processor and extends the pipeline registers to propagate analysis tags. To gain high analysis coverage, we rely on a population of users to run the program, sampling a different random set of variables during each new run. We show that we can achieve high coverage analysis at virtually no performance impact, even with a reasonably-sized population of users. In addition, our approach even scales to heavyweight debugging techniques by keeping per-user runtime overheads low despite performing traditionally costly analyses. Moreover, the low hardware cost of our implementation allows it to be easily distributed across large user populations, leading to a higher level of security analysis coverage than previously.
Joseph L. Greathouse, Ilya Wagner, David A. Ramos, Gautam Bhatnagar, Todd M. Austin, Valeria Bertacco, Seth Pettie
MICRO3