Thorough static analysis of device drivers

No abstract is available for this paper.

• Publication year

  2006

• Venue

  European Conference on Computer Systems

• Publication date

  2006-04-18

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1145/1217935.1217943
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Safe Hardware Access with the Xen Virtual Machine Monitor

  2007cited by this paper
• Termination proofs for systems code

  2006cited by this paper
• Binary rewriting and call interception for efficient runtime protection against buffer overflows

  2006cited by this paper
• Using Stålmarck's Algorithm to Prove Inequalities

  2005cited by this paper
• Abstraction Refinement for Termination

  2005cited by this paper
• Predicate Abstraction via Symbolic Decision Procedures

  2005cited by this paper
• The ASTREÉ Analyzer

  2005cited by this paper
• Cogent: Accurate Theorem Proving for Program Verification

  2005cited by this paper
• Model Checking x86 Executables with CodeSurfer/x86 and WPDS++

  2005cited by this paper
• Simplify: a theorem prover for program checking

  2005cited by this paper
• Symbolic Model Checking for Asynchronous Boolean Programs

  2005cited by this paper
• Linear Ranking with Reachability

  2005cited by this paper
• Improving the reliability of commodity operating systems

  2005cited by this paper
• Abstractions from proofs

  2004cited by this paper
• Predicate Abstraction of ANSI-C Programs Using SAT

  2004cited by this paper
• Refining Approximations in Software Predicate Abstraction

  2004cited by this paper
• KISS: keep it simple and sequential

  2004influential reference
• Zapato: Automatic Theorem Proving for Predicate Abstraction Refinement

  2004cited by this paper
• Model Checking One Million Lines of C Code

  2004cited by this paper
• Righting Software

  2004cited by this paper
• From symptom to cause: localizing errors in counterexample traces

  2003cited by this paper
• Modular verification of software components in C

  2003cited by this paper
• Lazy abstraction

  2002cited by this paper
• Extended static checking for Java

  2002cited by this paper
• A system and language for building system-specific, static analyses

  2002cited by this paper
• ESP: path-sensitive program verification in polynomial time

  2002cited by this paper
• Relative Completeness of Abstraction Refinement for Software Model Checking

  2002cited by this paper
• CCured: type-safe retrofitting of legacy code

  2002cited by this paper
• Enforcing high-level protocols in low-level software

  2001cited by this paper
• Automatically validating temporal safety properties of interfaces

  2001cited by this paper
• Boolean and Cartesian abstraction for model checking C programs

  2001cited by this paper
• Automatic predicate abstraction of C programs

  2001cited by this paper
• Bebop: a path-sensitive interprocedural dataflow engine

  2001cited by this paper
• An empirical study of operating systems errors

  2001cited by this paper
• Counterexample-guided Abstraction Reenement

  2000cited by this paper
• Enforceable security policies

  2000cited by this paper
• Unification-based pointer analysis with directional assignments

  2000cited by this paper
• Checking system rules using system-specific, programmer-written compiler extensions

  2000cited by this paper
• Counterexample-Guided Abstraction Refinement

  2000cited by this paper
• Bebop: A Symbolic Model Checker for Boolean Programs

  2000cited by this paper
• An Extended Static Checker for Modular-3

  1998cited by this paper
• An Automata-Theoretic Approach to Automatic Program Verification (Preliminary Report)

  1986cited by this paper
• Graph-Based Algorithms for Boolean Function Manipulation

  1986cited by this paper
• Proving the Correctness of Multiprocess Programs

  1977cited by this paper
• Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints

  1977cited by this paper

• Checking the HAL Interface Specification Continuously, Right from the Start

  2025cites this paper
• Moneta: Ex-Vivo GPU Driver Fuzzing by Recalling In-Vivo Execution States

  2025cites this paper
• DeepRadar: A cyber-defence interceptor for early warning and defusing malware injection attacks

  2025cites this paper
• Spinner: Detecting Locking Violations in the eBPF Runtime

  2025cites this paper
• Deprivileging Low-Level GPU Drivers Efficiently with User-Space Processes and CHERI Compartments

  2025cites this paper
• vkFlow: Automated Identification of Vulnerable Kernel Function Related to System Call

  2025cites this paper
• Temporal HAL-API Dependencies as a Gateway to Formal Embedded Software Development

  2025cites this paper
• Program Environment Fuzzing

  2024cites this paper
• Veld: Verified Linux Drivers

  2024cites this paper
• Studying the impact of risk assessment analytics on risk awareness and code review performance

  2024cites this paper
• Unlocking the Power of Environment Assumptions for Unit Proofs

  2024cites this paper
• Minimizing a Smartphone's TCB for Security-Critical Programs with Exclusively-Used, Physically-Isolated, Statically-Partitioned Hardware

  2023cites this paper
• Semantic-Informed Driver Fuzzing Without Both the Hardware Devices and the Emulators

  2022cites this paper
• A Personal Computer for a Distrustful World

  2022cites this paper
• SymFusion: Hybrid Instrumentation for Concolic Execution

  2022cites this paper
• Minimizing Trust with Exclusively-Used Physically-Isolated Hardware

  2022cites this paper
• ARBITRAR: User-Guided API Misuse Detection

  2021cites this paper
• A Review of Formal Methods applied to Machine Learning

  2021cites this paper
• Formal Proof of Node Level Trust Evaluation in Wireless Sensor Network

  2021cites this paper
• Model learning: a survey of foundations, tools and applications

  2021cites this paper
• Static Detection of Unsafe DMA Accesses in Device Drivers

  2021cites this paper
• Analysis of existing parallel programs verification technologies

  2020cites this paper
• Verifying correct usage of context-free API protocols

  2020cites this paper
• Fixing Vulnerabilities Automatically with Linters

  2020cites this paper
• Effective Detection of Sleep-in-atomic-context Bugs in the Linux Kernel

  2020cites this paper
• Defect Forecasting by Specification Mining Using Code Quality Metrics

  2020cites this paper
• OVER: overhauling vulnerability detection for iot through an adaptable and automated static analysis framework

  2020cites this paper
• A Program Verification based Approach to Find Data Race Vulnerabilities in Interrupt-driven Program

  2020cites this paper
• Continuous Reasoning for Real-World Program Analysis Tools

  2020cites this paper
• Rchecker: A CBMC-based Data Race Detector for Interrupt-driven Programs

  2020cites this paper
• Hierarchical Component Models

  2020cites this paper
• iDEA: Static Analysis on the Security of Apple Kernel Drivers

  2020cites this paper
• The application perspective of mutatoin testing

  2020cites this paper
• Chapter 2 High Assurance Software Lessons and Techniques

  2019cites this paper
• Hardware/Software Co-monitoring

  2019cites this paper
• Simple and precise static analysis of untrusted Linux kernel extensions

  2019cites this paper
• Detecting Callback Related Deep Vulnerabilities in Linux Device Drivers

  2019cites this paper
• The Case for I/O-Device-as-a-Service

  2019cites this paper
• Analyzing the Vulnerability in Open Source Software

  2019cites this paper
• PeriScope: An Effective Probing and Fuzzing Framework for the Hardware-OS Boundary

  2019cites this paper
• Testing-based Model Learning Approach for Legacy Components

  2019cites this paper
• Separation logic

  2019cites this paper
• Classifying False Positive Static Checker Alarms in Continuous Integration Using Convolutional Neural Networks

  2019cites this paper
• Model Checking Embedded Control Software using OS-in-the-Loop CEGAR

  2019cites this paper
• SAT-Based Model Checking

  2018cites this paper
• Lessons from building static analysis tools at Google

  2018cites this paper
• Chapter Two - Advances in Software Model Checking

  2018cites this paper
• A two-step approach for pattern-based API-call constraint checking

  2018cites this paper
• Model Learning: A Survey on Foundation, Tools and Applications

  2018cites this paper
• A Survey of Formal Techniques for Hardware/Software Co-verification

  2018cites this paper
• Компонентная верификация операционных систем

  2018cites this paper
• We Need a Testability Transformation Semantics

  2018cites this paper
• Increasing Efficiency in Data Flow Oriented Model Driven Software Development for Softcore Processors

  2018cites this paper
• From Start-ups to Scale-ups: Opportunities and Open Problems for Static and Dynamic Program Analysis

  2018cites this paper
• DSAC: Effective Static Analysis of Sleep-in-Atomic-Context Bugs in Kernel Modules

  2018cites this paper
• FaultVisor2: Testing Hypervisor Device Drivers Against Real Hardware Failures

  2018cites this paper
• Static verification for memory safety of Linux kernel drivers

  2018cites this paper
• Statistical Reconstruction of Class Hierarchies in Binaries

  2018cites this paper
• Charm: Facilitating Dynamic Analysis of Device Drivers of Mobile Systems

  2018cites this paper
• Mutation Testing for Physical Computing

  2018cites this paper
• Formal Reasoning About the Security of Amazon Web Services

  2018cites this paper
• The past, present, and future(s): verifying temporal software properties

  2018cites this paper
• Continuous Reasoning: Scaling the impact of formal methods

  2018influential citation
• Exploring the Augmentation of Fuzzing Techniques with Interface Awareness

  2017cites this paper
• Reverse engineering source code: Empirical studies of limitations and opportunities

  2017cites this paper
• VERIFICATION OF OPERATING SYSTEM COMPONENTS

  2017cites this paper
• Interactive Runtime Verification — When Interactive Debugging Meets Runtime Verification

  2017cites this paper
• DIFUZE: Interface Aware Fuzzing for Kernel Drivers

  2017cites this paper
• Verifying Increasingly Expressive Temporal Logics for Infinite-State Systems

  2017cites this paper
• BabelView: Evaluating the Impact of Code Injection Attacks in Mobile Webviews

  2017cites this paper
• Modular Semi-automatic Formal Verification of Critical Systems Software ; Modulaire halfautomatische formele verificatie van kritische systeemsoftware

  2017influential citation
• Assisting Malware Analysis with Symbolic Execution: A Case Study

  2017cites this paper
• System-Level Non-interference of Constant-Time Cryptography. Part I: Model

  2017cites this paper
• Extending programs with debug-related features, with application to hardware development

  2017cites this paper
• Page Fault Support for Network Controllers

  2017cites this paper
• Interactive Runtime Verification

  2017cites this paper
• A Framework for Recognition and Confronting of Obfuscated Malwares Based on Memory Dumping and Filter Drivers

  2017cites this paper
• Support for learning while debugging in a distributed visual programming language

  2017cites this paper
• Обзор подходов к моделированию памяти в инструментах статической верификации

  2017cites this paper
• DR. CHECKER: A Soundy Analysis for Linux Kernel Drivers

  2017influential citation
• Securing software systems by preventing information leaks

  2017cites this paper
• Improving the Reliability of the Operating System Inside a VM

  2016cites this paper
• True IOMMU Protection from DMA Attacks: When Copy is Faster than Zero Copy

  2016cites this paper
• Enforcing Kernel Security Invariants with Data Flow Integrity.

  2016cites this paper
• Prescriptive Safety-Checks through Automated Proofs for Control-Flow Integrity

  2016cites this paper
• Preventing exploits against memory corruption vulnerabilities

  2016cites this paper
• Model-Based API-Call Constraint Checking for Automotive Control Software

  2016cites this paper
• A methodology for trustworthy file systems

  2016cites this paper
• On-the-fly decomposition of specifications in software model checking

  2016cites this paper
• Viola: Trustworthy Sensor Notifications for Enhanced Privacy on Mobile Systems

  2016cites this paper
• Reviewing and Classification of Software Model Checking Tools

  2016cites this paper
• Improving systems software security through program analysis and instrumentation

  2016cites this paper
• Ahead of time static analysis for automatic generation of debugging interfaces to the Linux kernel

  2016cites this paper
• Testing Error Handling Code in Device Drivers Using Characteristic Fault Injection

  2016cites this paper
• Active learning for extended finite state machines

  2016cites this paper
• A Case for Static Analysis of Linux to Find Faults in Interrupt Request Handlers

  2016influential citation
• Scalable techniques for analysing and testing asynchronous software systems

  2016cites this paper
• Toward Compositional Verification of Interruptible OS Kernels and Device Drivers

  2016cites this paper
• Light-Weight API-Call Safety Checking for Automotive Control Software Using Constraint Patterns

  2016cites this paper
• Comparison of Path Exploration and Model Checking Techniques for Checking Automotive API Call Safety

  2016cites this paper