• Recent & Upcoming Talks
    • Example Talk
  • Projects
  • Publications
    • Adaptive Quotient Filters
    • File System Aging
    • IONIA:High-Performance Replication for Modern Disk-based KV Stores
    • Mosaic Pages: Big TLB Reach with Small Pages
    • Proactive splitting and merging of nodes in a B$ɛ$-tree
    • Reduced bandwidth queries in B e-trees using approximate membership query data structures
    • IcebergHT: High Performance Hash Tables Through Stability and Low Associativity
    • Mosaic pages: Big TLB reach with small pages
    • SplinterDB and Maplets: Improving the Tradeoffs in Key-Value Store Compaction Policy
    • Range lookup operations for B$ɛ$-trees using update messages
    • Merge updates for key value stores
    • Optimizing operations on b e-trees stored on solid state media
    • An incrementally updatable and scalable system for large-scale sequence search using the Bentley--Saxe transformation
    • BetrFS: a compleat file system for commodity SSDs
    • IcebergHT: High performance PMEM hash tables through stability and low associativity
    • Using External Memory to Improve Cyber-Security Stream Monitoring.
    • When Are Cache-Oblivious Algorithms Cache Adaptive? A Case Study of Matrix Multiplication and Sorting
    • Write-Optimized Algorithms for Cybersecurity Stream Monitoring.
    • Large range lookups for Bϵ-tree
    • Mirrored write ahead logs for data storage system
    • Advanced Data Structures for Monitoring Cyber Streams.
    • An incrementally updatable and scalable system for large-scale sequence search using LSM trees
    • Copy-on-abundant-write for nimble file system clones
    • External-memory Dictionaries in the Affine and PDAM Models
    • Paging and the address-translation problem
    • Timely Reporting of Heavy Hitters Using External Memory
    • Vector quotient filters: Overcoming the time/space trade-off in filter design
    • System and method for managing transactions for multiple data store nodes without a central log
    • $$SplinterDB$$: closing the bandwidth gap for $$NVMe$$$$Key-Value$$ stores
    • An efficient, scalable, and exact representation of high-dimensional color information enabled using de Bruijn graph search
    • Closing the gap between cache-oblivious and cache-adaptive analysis
    • Flushing without cascades
    • How to copy files
    • How to Not Copy Files
    • Storage Systems are Distributed Systems (So Verify Them That $$Way!$$)
    • Timely reporting of heavy hitters using external memory
    • System and method for managing storage transaction requests
    • Small Refinements to the DAM Can Have Big Consequences for Data-Structure Design
    • An example preprint / working paper
    • Engineering a high-performance GPU B-Tree
    • Filesystem aging:$$It’s$$ more usage than fullness
    • Optimal ball recycling
    • Small refinements to the DAM can have big consequences for data-structure design
    • Theoretical Foundations of Storage Systems (Dagstuhl Seminar 19111)
    • Advanced data structures for improved cyber resilience and awareness in untrusted environments: LDRD report
    • Bloom filters, adaptivity, and the dictionary problem
    • Efficient directory mutations in a full-path-indexed file system
    • Mantis: a fast, small, and exact large-scale sequence-search index
    • Mantis: A fast, small, and exact large-scale sequence-search index
    • Squeakr: an exact and approximate k-mer counting system
    • The Full Path to $$Full-Path$$ Indexing
    • The Online Event-Detection Problem
    • A fast x86 implementation of select
    • A general-purpose counting filter: Making every bit count
    • deBGR: an efficient and near-exact representation of the weighted de Bruijn graph
    • File systems fated for senescence? nonsense, says science!
    • How to fragment your file system
    • Write-optimized skip lists
    • Writes wrought right, and other adventures in file system optimization
    • Cache-Adaptive Analysis (Full Version)
    • Poster: Games Without Frontiers: Investigating Video Games as a Covert Channel
    • Anti-persistence on persistent storage: History-independent sparse tables and dictionaries
    • Cache-adaptive analysis
    • Games without frontiers: Investigating video games as a covert channel
    • Lazy analytics: Let other queries do the work for you
    • Optimizing every operation in a write-optimized file system
    • The i/o complexity of computing prime tables
    • An example journal article
    • BetrFS: A Right-Optimized Write-Optimized File System
    • $$BetrFS$$: A $$Right-Optimized$$$$Write-Optimized$$ file system
    • An introduction to B-trees and write-optimization
    • Fixing races for good: Portable and reliable unix file-system race detection
    • Tracking Network Events with Write Optimized Data Structures
    • Tracking Network Events with Write Optimized Data Structures
    • A systematic approach to developing and evaluating website fingerprinting defenses
    • Cache-adaptive algorithms
    • Cs-buflo: A congestion sensitive website fingerprinting defense
    • Effective attacks and provable defenses for website fingerprinting
    • Glove: A bespoke website fingerprinting defense
    • How Best to Handle a Dicey Situation
    • New approaches to website fingerprinting defenses
    • An example conference paper
    • Gone, But Not Forgotten: The Current State of Private Computing
    • The password allocation problem: strategies for reusing passwords effectively
    • CAWDOR: compiler assisted worm defense
    • Touching from a distance: Website fingerprinting attacks and defenses
    • Types and Access Controls for Cross-Domain Security in Flash
    • Don’t Thrash: How to Cache Your Hash in Flash
    • Don't Thrash: How to Cache your Hash on Flash
    • Homomorphic signatures for digital photographs
    • Implementing a key recovery attack on the high-bandwidth digital content protection protocol
    • Language of vandalism: Improving wikipedia vandalism detection via stylometric analysis
    • Phorcefield: A phish-proof password ceremony
    • Text classification for data loss prevention
    • Prevention and Reaction: Defending Privacy in the Web 2.0
    • Wiki Vandalysis-Wikipedia Vandalism Analysis
    • Exploiting unix file-system races via algorithmic complexity attacks
    • iTag: a personalized blog tagger
    • Pre-patched software
    • Usable privacy controls for blogs
    • Methods, apparatus, and program products for inferring service usage
    • A practical mimicry attack against powerful system-call monitors
    • Flow-Insensitive Type Qualifiers
    • Methods, apparatus, and program products for inferring service usage
    • Deflation-secure web metering
    • Efficient and accurate detection of integer-based attacks
    • More content-less control: Access control in the web 2.0
    • RICH: Automatically protecting against integer-based vulnerabilities
    • Verifying security properties using type-qualifier inference
    • Fixing races for fun and profit: how to abuse atime
    • Finding user/kernel pointer bugs with type inference.
    • Did Filiol Break AES?
    • A cryptanalysis of the high-bandwidth digital content protection system
    • Checking Linux kernel user-space pointer handling with $$CQual$$
    • FAIR: Fair audience inference
    • Homomorphic signature schemes
    • Multiplicative differentials
    • New Approaches to Data Location
    • On union-closed families, I
    • Poster: Maxwell: User-Driven Information Flow Control for Android
  • Blog
    • 🎉 Easily create your own simple yet highly customizable blog
    • 🧠 Sharpen your thinking with a second brain
    • 📈 Communicate your results effectively with the best data visualizations
    • 👩🏼‍🏫 Teach academic courses
    • ✅ Manage your projects
  • Projects
    • Pandas
    • PyTorch
    • scikit-learn
  • Experience
  • Teaching
    • Learn JavaScript
    • Learn Python

Verifying security properties using type-qualifier inference

Jan 1, 2006·
Robert Timothy Johnson
· 0 min read
Cite
Type
Thesis
Last updated on Jan 1, 2006
← RICH: Automatically protecting against integer-based vulnerabilities Jan 1, 2007
Fixing races for fun and profit: how to abuse atime Jan 1, 2005 →

Published with Hugo Blox Builder — the free, open source website builder that empowers creators.