# Denis Efremov

> System Developer and Formal Verification Engineer. Linux kernel contributor, Ksplice live patching, formal methods researcher.

## Research Areas

- Linux kernel development and security
- Live patching (Ksplice)
- Formal verification (Frama-C, Coq, Event-B, ACSL)
- Semantic code analysis (Coccinelle)
- Operating system security and access control

## Links

- Homepage: https://denis.efremov.cv/
- ORCID: https://orcid.org/0000-0002-9916-056X
- Google Scholar: https://scholar.google.com/citations?user=Tn954SsAAAAJ
- GitHub: https://github.com/evdenis
- DBLP: https://dblp.org/pid/118/1171.html
- LinkedIn: https://www.linkedin.com/in/evdenis

## Professional Experience

- **Consulting Software Engineer, Oracle, Dubai** (Jun 2022 - Present): Led design and implementation of Ksplice live patching engine features. Developed QA and performance testing frameworks.
- **Principal Developer, Oracle, Moscow** (Mar 2021 - May 2022): Linux kernel developer on Ksplice team. Runtime update preparation, RHEL maintenance, kernel QA/testing/fuzzing.
- **Researcher / Developer / Formal Verification Engineer, ISP RAS, Moscow** (Jul 2011 - Mar 2021): Formal specification and verification of Linux security modules with Frama-C/Coq/Event-B. Contributed to GOST R 59453.4-2025 standard.
- **Research Intern, Fraunhofer FOKUS, Berlin** (Jan 2019 - Apr 2019): Vessedia project, ACSL-By-Example.
- **Software Developer, Yandex, Moscow** (Oct 2017 - May 2018): Backend for Partner Interface 2.0.
- **Software Developer, Google Summer of Code** (2012, 2013): Concolic testing for Linux kernel file system drivers; Linux kernel API models for LDV.

## Education

- **PhD Candidate**, Higher School of Economics, Moscow (2015-2018): Verification Methods for Software Systems With Access Control Functions Based on Formal Models
- **Specialist (BSc + MSc equivalent)**, M. V. Lomonosov Moscow State University (2006-2011): Mathematics and System Programming. Diploma: AMD-V SVM-based hardware virtualization firewall.

## Skills

- **Languages**: C, Perl, Python, ACSL, Shell
- **Tools**: Ansible, QEMU, Git, GDB, GCC, LibFuzzer, Coccinelle, Frama-C, Why3, Coq, Event-B, ProB
- **Linux Kernel**: Syzkaller, SystemTap, gcov

## Publications

### Overview of Hardening Mechanisms in Operating Systems and User Applications

- **Authors**: D.V. Efremov, A.K. Petrenko, B.A. Pozin, V.A. Semenov
- **Venue**: Proceedings of ISP RAS, 2025
- **Volume**: 37, No. 3
- **Pages**: 325–354
- **DOI**: https://doi.org/10.15514/ISPRAS-2025-37(3)-23
- **Abstract**: This paper presents a systematic review of hardening mechanisms for operating systems and user applications. Various types of protection mechanisms are discussed, including memory protection mechanisms, hardware stack protection, dynamic memory protection, address space randomization, control flow protection, and system integrity protection. The principles of these mechanisms, their effectiveness, and their impact on system performance are analyzed in detail. Special attention is given to the implementation of protective mechanisms in modern operating systems, particularly in the Linux kernel.

### Methods of Runtime Verification of Industrial Information Security Tools Based on Formal Access Control Models

- **Authors**: A.K. Petrenko, P.N. Devyanin, D.V. Efremov, A.A. Karnov, E.V. Kornykhin, V.V. Kuliamin, A.V. Khoroshilov
- **Venue**: Proceedings of ISP RAS, 2025
- **Volume**: 37, No. 3
- **Pages**: 277–290
- **DOI**: https://doi.org/10.15514/ISPRAS-2025-37(3)-19
- **Abstract**: The article addresses runtime verification methods for security protection mechanisms in software systems. It presents a technology combining formal testing techniques with formal access control models and functional specifications, designed for practical industrial application. The approach is illustrated through the new GOST R 59453.4-2025 standard on verifying information security tools implementing access control policies.

### Runtime Verification of Industrial Information Security Tools Based on Formal Access Control Models

- **Authors**: A.K. Petrenko, D.V. Efremov, E.V. Kornykhin, V.V. Kuliamin, V.A. Semenov
- **Venue**: Software & Systems, 2025
- **Volume**: 38, No. 2
- **Pages**: 374–380
- **DOI**: https://doi.org/10.15827/0236-235X.150.374-380
- **Abstract**: The work addresses verification methodology for information security mechanisms against formal security models. The authors propose using runtime verification to compare execution traces between an implemented security system and its formal model.

### Runtime Verification of Operating Systems Based on Abstract Models

- **Authors**: D.V. Efremov, V.V. Kopach, E.V. Kornykhin, V.V. Kuliamin, A.K. Petrenko, A.V. Khoroshilov, I.V. Shchepetkov
- **Venue**: Programming and Computer Software, 2023
- **Volume**: 49, No. 7
- **Pages**: 559–565
- **DOI**: https://doi.org/10.1134/S0361768823070034
- **Abstract**: High complexity of a modern operating system (OS) requires to use complex models and high-level specification languages to describe even separated aspects of OS functionality, e.g., security functions. Use of such models in conformance verification of modeled OS needs to establish rather complex relation between elements of OS implementation and elements of the model. In this paper we present a method to establish and support such a relation, which can be effectively used in testing and runtime verification/monitoring of OS. The method described was used successfully in testing and monitoring of Linux OS core components on conformance to Event-B models.

### Runtime Verification of Operating Systems Based on Abstract Models

- **Authors**: D.V. Efremov, V.V. Kopach, E.V. Kornykhin, V.V. Kuliamin, A.K. Petrenko, A.V. Khoroshilov, I.V. Shchepetkov
- **Venue**: Proceedings of ISP RAS, 2021
- **Volume**: 33, No. 6
- **Pages**: 15–26
- **DOI**: https://doi.org/10.15514/ISPRAS-2021-33(6)-2
- **Abstract**: High complexity of a modern operating system (OS) requires to use complex models and high-level specification languages to describe even separated aspects of OS functionality, e.g., security functions. Use of such models in conformance verification of modeled OS needs to establish rather complex relation between elements of OS implementation and elements of the model. In this paper we present a method to establish and support such a relation, which can be effectively used in testing and runtime verification/monitoring of OS. The method described was used successfully in testing and monitoring of Linux OS core components on conformance to Event-B models.

### Monitoring and Testing Based on Multi-Level Program Specifications

- **Authors**: A.K. Petrenko, D.V. Efremov, E.V. Kornykhin, V.V. Kuliamin, A.V. Khoroshilov, I.V. Shchepetkov
- **Venue**: Proceedings of ISP RAS, 2020
- **Volume**: 32, No. 6
- **Pages**: 7–18
- **DOI**: https://doi.org/10.15514/ISPRAS-2020-32(6)-1
- **Abstract**: The paper addresses building multi-level specifications for formal verification. Testing using formal models should employ the same specifications used in formal verification. The authors examine various development methods, integration possibilities, and constraints for test and monitoring systems.

### Runtime Verification of Linux Kernel Security Module

- **Authors**: Denis Efremov, Ilya Shchepetkov
- **Venue**: FM 2019 International Workshops, 2020
- **Volume**: 12233
- **Pages**: 185–199
- **DOI**: https://doi.org/10.1007/978-3-030-54997-8_12
- **Abstract**: The Linux kernel is one of the most important Free/Libre Open Source Software (FLOSS) projects. It is installed on billions of devices all over the world, which process various sensitive, confidential or simply private data. It is crucial to establish and prove its security properties. This work-in-progress paper presents a method to verify the Linux kernel for conformance with an abstract security policy model written in the Event-B specification language. The method is based on system call tracing and aims at checking that the results of system call execution do not lead to accesses that violate security policy requirements.

### Modeling and Verification of Access Control Security Policies in Operating Systems

- **Authors**: P.N. Devyanin, D.V. Efremov, V.V. Kuliamin, A.K. Petrenko, A.V. Khoroshilov, I.V. Shchepetkov
- **Venue**: Goryachaya Liniya – Telekom, 2019
- **Pages**: 214

### ACSL by Example: Towards a Formally Verified Standard Library

- **Authors**: Jens Gerlach, Denis Efremov, Tim Sikatzki et al.
- **Venue**: Fraunhofer FOKUS, 2019

### Deductive Verification of Unmodified Linux Kernel Library Functions

- **Authors**: Denis Efremov, Mikhail Mandrykin, Alexey Khoroshilov
- **Venue**: ISoLA 2018, 2018
- **Volume**: 11245
- **Pages**: 216–234
- **DOI**: https://doi.org/10.1007/978-3-030-03421-4_15
- **Abstract**: This paper presents results from the development and evaluation of a deductive verification benchmark consisting of 26 unmodified Linux kernel library functions implementing conventional memory and string operations. The formal contract of the functions was extracted from their source code and was represented in the form of preconditions and postconditions. The correctness of 23 functions was completely proved using AstraVer toolset, although success for 11 functions was achieved using 2 new specification language constructs. Another 2 functions were proved after a minor modification of their source code, while the final one cannot be completely proved using the existing memory model.

### Lemma Functions for Frama-C: C Programs as Proofs

- **Authors**: Grigoriy Volkov, Mikhail Mandrykin, Denis Efremov
- **Venue**: ISPRAS Open 2018, 2018
- **Pages**: 31–38
- **DOI**: https://doi.org/10.1109/ISPRAS.2018.00012
- **Abstract**: The paper presents an auto-active verification technique developed within the Frama-C framework. It details the lemma functions method and presents the corresponding ACSL extension, its implementation in Frama-C, and evaluation on a set of string-manipulating functions from the Linux kernel.

### Formal Verification of Linux Kernel Library Functions

- **Authors**: Denis Efremov, Mikhail Mandrykin
- **Venue**: Proceedings of ISP RAS, 2017
- **Volume**: 29, No. 6
- **Pages**: 49–76
- **DOI**: https://doi.org/10.15514/ISPRAS-2017-29(6)-3

### Construction of the Operating System Kernel

- **Authors**: D.V. Efremov, N.Yu. Komarov, A.V. Khoroshilov
- **Venue**: MSU/MAKS Press, 2015
- **Pages**: 160

### Tools Support for Linux Kernel Deductive Verification Workflow

- **Authors**: Denis Efremov, Nikita Komarov
- **Venue**: SYRCoSE 2014, 2014
- **Volume**: 8, No. 6
- **Pages**: 39–44
- **DOI**: https://doi.org/10.15514/SYRCOSE-2014-8-6
- **Abstract**: The paper examines formal verification of a Linux kernel security module through deductive methods. The authors describe their chosen toolset (Frama-C, Why, Jessie), the verification workflow, and auxiliary tools they developed. Key challenges addressed include handling C language extensions, managing dependencies with kernel headers, and coordinating specifications development during active code development.

### Sevigator: Network Confinement of Malware Applications and Untrusted Operating Systems

- **Authors**: Denis Efremov, Nikolay Pakulin
- **Venue**: SECRYPT 2012, 2012
- **Pages**: 395–398
- **DOI**: https://doi.org/10.5220/0004070103950398
- **Abstract**: The paper presents Sevigator -- a toolkit for network confinement where only trusted applications gain access to the local network while other applications and even the OS kernel have no networking at all. Sevigator is based on hardware virtualization support: a custom hypervisor hides network interface card from the OS kernel and delegates network-based system calls of trusted applications to a dedicated service virtual machine.

### Protection of the Applications' Privacy Running Untrusted Operating System

- **Authors**: Denis Efremov
- **Venue**: APSSE 2011, 2011

### An Approach to On-the-Fly Activation and Deactivation of Virtualization-Based Security Systems

- **Authors**: Denis Efremov, Pavel Iakovenko
- **Venue**: SYRCoSE 2010, 2010
- **Volume**: 4
- **Pages**: 157–161
- **DOI**: https://doi.org/10.15514/SYRCOSE-2010-4-31
- **Abstract**: The authors present a method for on-the-fly activation and deactivation of hardware virtualization based security systems that protect applications running under untrusted operating systems. The approach addresses resource reservation from the OS for hypervisor and additional virtual machines, while considering threats from malicious startup and shutdown environments.

## Key Projects

- [CVEhound](https://github.com/evdenis/cvehound) - Scan Linux kernel sources for known CVEs using Coccinelle semantic patches. State Registration No. RU 2021663474.
- [CruelKernel](https://github.com/CruelKernel) - Custom kernel for Samsung Galaxy S10/Note10 series with browser-based builds via GitHub Actions.
- [VerKer](https://github.com/evdenis/verker) - Formal verification benchmark for Linux kernel library functions (Frama-C/ACSL).
- [Spec-Utils](https://github.com/evdenis/spec-utils) - Perl tools for writing ACSL specifications for Linux kernel code.
- [adb_root](https://github.com/evdenis/adb_root) - Magisk module enabling ADB root access on Android 10+.
- [lsm_bpf_check_argc0](https://github.com/evdenis/lsm_bpf_check_argc0) - LSM BPF module to block pwnkit (CVE-2021-4034) like exploits.

## Linux Kernel Maintainership

- **Floppy driver maintainer** since Jul 2019 (listed in kernel MAINTAINERS file)
- Coccinelle semantic patch rules: kfree_mismatch, flexible_array, kvmalloc, excluded_middle, uninitialized_var, kobj_to_dev, kzfree, array_size_dup, device_attr_show
- CVE fixes: CVE-2019-14284, CVE-2019-14283
- Syzkaller fuzzing rules: integrity (IMA/EVM), smack, floppy, cdrom, i2c
- Full commit list: https://git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git/log/?qt=grep&q=Denis+Efremov