# 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

## Publications

- Overview of Hardening Mechanisms in Operating Systems and User Applications. Proceedings of ISP RAS, 2025. https://doi.org/10.15514/ISPRAS-2025-37(3)-23
- Methods of Runtime Verification of Industrial Information Security Tools Based on Formal Access Control Models. Proceedings of ISP RAS, 2025. https://doi.org/10.15514/ISPRAS-2025-37(3)-19
- Runtime Verification of Industrial Information Security Tools Based on Formal Access Control Models. Software & Systems, 2025. https://doi.org/10.15827/0236-235X.150.374-380
- Runtime Verification of Operating Systems Based on Abstract Models. Programming and Computer Software, 2023. https://doi.org/10.1134/S0361768823070034
- Runtime Verification of Operating Systems Based on Abstract Models. Proceedings of ISP RAS, 2021. https://doi.org/10.15514/ISPRAS-2021-33(6)-2
- Monitoring and Testing Based on Multi-Level Program Specifications. Proceedings of ISP RAS, 2020. https://doi.org/10.15514/ISPRAS-2020-32(6)-1
- Runtime Verification of Linux Kernel Security Module. FM 2019 International Workshops, 2020. https://doi.org/10.1007/978-3-030-54997-8_12
- Modeling and Verification of Access Control Security Policies in Operating Systems. Goryachaya Liniya – Telekom, 2019.
- ACSL by Example: Towards a Formally Verified Standard Library. Fraunhofer FOKUS, 2019.
- Deductive Verification of Unmodified Linux Kernel Library Functions. ISoLA 2018, 2018. https://doi.org/10.1007/978-3-030-03421-4_15
- Lemma Functions for Frama-C: C Programs as Proofs. ISPRAS Open 2018, 2018. https://doi.org/10.1109/ISPRAS.2018.00012
- Formal Verification of Linux Kernel Library Functions. Proceedings of ISP RAS, 2017. https://doi.org/10.15514/ISPRAS-2017-29(6)-3
- Construction of the Operating System Kernel. MSU/MAKS Press, 2015.
- Tools Support for Linux Kernel Deductive Verification Workflow. SYRCoSE 2014, 2014. https://doi.org/10.15514/SYRCOSE-2014-8-6
- Sevigator: Network Confinement of Malware Applications and Untrusted Operating Systems. SECRYPT 2012, 2012. https://doi.org/10.5220/0004070103950398
- Protection of the Applications' Privacy Running Untrusted Operating System. APSSE 2011, 2011.
- An Approach to On-the-Fly Activation and Deactivation of Virtualization-Based Security Systems. SYRCoSE 2010, 2010. https://doi.org/10.15514/SYRCOSE-2010-4-31

## Linux Kernel Maintainership

- Floppy driver maintainer since Jul 2019 (listed in MAINTAINERS)
- 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

## Key Projects

- [CVEhound](https://github.com/evdenis/cvehound) - Scan Linux kernel sources for known CVEs using Coccinelle semantic patches
- [CruelKernel](https://github.com/CruelKernel) - Custom kernel for Samsung Galaxy S10/Note10 with browser-based builds
- [VerKer](https://github.com/evdenis/verker) - Formal verification benchmark for Linux kernel library functions
- [Spec-Utils](https://github.com/evdenis/spec-utils) - Perl tools for writing ACSL specifications for Linux kernel code