Denis Efremov

Experience

Jun 2022 – Present Consulting Software Engineer — Oracle, Dubai

Led design and implementation of Ksplice's live patching engine features, enabling zero-downtime security updates across Oracle Linux, RHEL, and Ubuntu. Developed QA and performance testing frameworks. Established engineering best practices. Collaborated with Oracle Cloud Infrastructure teams.

Mar 2021 – May 2022 Principal Developer — Oracle, Moscow

Linux kernel developer on the Ksplice team: runtime update preparation, RHEL EL9/EL10 maintenance, kernel QA/testing/fuzzing, CVE tracking and security commit tagging.

Jul 2011 – Mar 2021 Researcher / Developer / Formal Verification Engineer — ISP RAS, Moscow

Contributed to GOST R 59453.4-2025 standard on verification of access control security tools. Formal specification and verification of Linux security modules (AstraLinux, Elbrus distros) with Frama-C/Coq/Event-B. Developed ACSL specification tools and fuzzing rules. Enabled RusBiTech to pass highest-level government certifications (FSB and FSTEK).

Jan 2019 – Apr 2019 Research Intern — Fraunhofer FOKUS, Berlin

System Quality Center lab. Vessedia project (formal verification of IoT OS Contiki) and ACSL-By-Example. Resulted in collaboration agreement between ISP RAS and Fraunhofer FOKUS.

Oct 2017 – May 2018 Software Developer — Yandex, Moscow

Backend team for Partner Interface 2.0 (Google AdSense analog): REST API for video/indoor ad blocks, statistics export, action logs refactoring.

2013, 2012 Software Developer — Google Summer of Code

2013: Concolic testing tool for Linux kernel file system driver verification (S2E-based). 2012: Formalized 12 Linux kernel API models for Linux Driver Verification tool.

Education

PhD Candidate — Higher School of Economics, Moscow 2015 – 2018 · Physics and Mathematics

Verification Methods for Software Systems With Access Control Functions Based on Formal Models

Specialist — Lomonosov Moscow State University (MSU) 2006 – 2011 · Mathematics and System Programming

Specialist degree (BSc + MSc equivalent). 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

Distributions Gentoo Fedora Debian/Ubuntu

Publications

ORCID Google Scholar DBLP Semantic Scholar ResearchGate BibTeX BibLaTeX

Academic (17)

2025

Overview of Hardening Mechanisms in Operating Systems and User Applications (Russian)
Efremov D.V., Petrenko A.K., Pozin B.A., Semenov V.A. Proceedings of ISP RAS, Vol. 37, No. 3, pp. 325–354 · DOI · PDF

BibTeXBibLaTeX

@article{efremov_hardening_overview_2025,
    author = {Efremov, D. V. and Petrenko, A. K. and Pozin, B. A. and Semenov, V. A.},
    title = {Overview of Hardening Mechanisms in Operating Systems and User Applications},
    journal = {Proceedings of the Institute for System Programming of the RAS},
    year = {2025},
    volume = {37},
    number = {3},
    pages = {325--354},
    doi = {10.15514/ISPRAS-2025-37(3)-23},
    issn = {2079-8156},
    url = {https://ispranproceedings.elpub.ru/jour/article/view/1954}
}

@article{efremov_hardening_overview_2025,
    author = {Efremov, D. V. and Petrenko, A. K. and Pozin, B. A. and Semenov, V. A.},
    title = {Overview of Hardening Mechanisms in Operating Systems and User Applications},
    journaltitle = {Proceedings of the Institute for System Programming of the RAS},
    date = {2025},
    volume = {37},
    number = {3},
    pages = {325--354},
    doi = {10.15514/ISPRAS-2025-37(3)-23},
    issn = {2079-8156},
    url = {https://ispranproceedings.elpub.ru/jour/article/view/1954}
}

Methods of Runtime Verification of Industrial Information Security Tools Based on Formal Access Control Models (Russian)
Petrenko A.K., Devyanin P.N., Efremov D.V. et al. Proceedings of ISP RAS, Vol. 37, No. 3, pp. 277–290 · DOI · PDF

BibTeXBibLaTeX

@article{petrenko_rv_methods_isp_2025,
    author = {Petrenko, A. K. and Devyanin, P. N. and Efremov, D. V. and Karnov, A. A. and Kornykhin, E. V. and Kuliamin, V. V. and Khoroshilov, A. V.},
    title = {Methods of Runtime Verification of Industrial Information Security Tools Based on Formal Access Control Models},
    journal = {Proceedings of the Institute for System Programming of the RAS},
    year = {2025},
    volume = {37},
    number = {3},
    pages = {277--290},
    doi = {10.15514/ISPRAS-2025-37(3)-19},
    issn = {2079-8156},
    url = {https://ispranproceedings.elpub.ru/jour/article/view/1949}
}

@article{petrenko_rv_methods_isp_2025,
    author = {Petrenko, A. K. and Devyanin, P. N. and Efremov, D. V. and Karnov, A. A. and Kornykhin, E. V. and Kuliamin, V. V. and Khoroshilov, A. V.},
    title = {Methods of Runtime Verification of Industrial Information Security Tools Based on Formal Access Control Models},
    journaltitle = {Proceedings of the Institute for System Programming of the RAS},
    date = {2025},
    volume = {37},
    number = {3},
    pages = {277--290},
    doi = {10.15514/ISPRAS-2025-37(3)-19},
    issn = {2079-8156},
    url = {https://ispranproceedings.elpub.ru/jour/article/view/1949}
}

Runtime Verification of Industrial Information Security Tools Based on Formal Access Control Models (Russian)
Petrenko A.K., Efremov D.V., Kornykhin E.V., Kuliamin V.V., Semenov V.A. Software & Systems, Vol. 38, No. 2, pp. 374–380 · DOI · PDF

BibTeXBibLaTeX

@article{petrenko_rv_methods_pps_2025,
    author = {Petrenko, A. K. and Efremov, D. V. and Kornykhin, E. V. and Kuliamin, V. V. and Semenov, V. A.},
    title = {Runtime Verification of Industrial Information Security Tools Based on Formal Access Control Models},
    journal = {Software \& Systems},
    year = {2025},
    volume = {38},
    number = {2},
    pages = {374--380},
    doi = {10.15827/0236-235X.150.374-380},
    issn = {0236-235X},
    url = {https://cyberleninka.ru/article/n/dinamicheskaya-verifikatsiya-promyshlennyh-sredstv-zaschity-informatsii-na-osnove-formalnyh-modeley-upravleniya-dostupom}
}

@article{petrenko_rv_methods_pps_2025,
    author = {Petrenko, A. K. and Efremov, D. V. and Kornykhin, E. V. and Kuliamin, V. V. and Semenov, V. A.},
    title = {Runtime Verification of Industrial Information Security Tools Based on Formal Access Control Models},
    journaltitle = {Software \& Systems},
    date = {2025},
    volume = {38},
    number = {2},
    pages = {374--380},
    doi = {10.15827/0236-235X.150.374-380},
    issn = {0236-235X},
    url = {https://cyberleninka.ru/article/n/dinamicheskaya-verifikatsiya-promyshlennyh-sredstv-zaschity-informatsii-na-osnove-formalnyh-modeley-upravleniya-dostupom}
}

2023

Runtime Verification of Operating Systems Based on Abstract Models
Efremov D.V., Kopach V.V., Kornykhin E.V., Kuliamin V.V., Petrenko A.K., Khoroshilov A.V., Shchepetkov I.V. Programming and Computer Software, Vol. 49, No. 7, pp. 559–565 · DOI · PDF

BibTeXBibLaTeX

@article{efremov_rv_pcs_2023,
    author = {Efremov, D. V. and Kopach, V. V. and Kornykhin, E. V. and Kuliamin, V. V. and Petrenko, A. K. and Khoroshilov, A. V. and Shchepetkov, I. V.},
    title = {Runtime Verification of Operating Systems Based on Abstract Models},
    journal = {Programming and Computer Software},
    year = {2023},
    volume = {49},
    number = {7},
    pages = {559--565},
    doi = {10.1134/S0361768823070034},
    issn = {0361-7688},
    publisher = {Pleiades Publishing}
}

@article{efremov_rv_pcs_2023,
    author = {Efremov, D. V. and Kopach, V. V. and Kornykhin, E. V. and Kuliamin, V. V. and Petrenko, A. K. and Khoroshilov, A. V. and Shchepetkov, I. V.},
    title = {Runtime Verification of Operating Systems Based on Abstract Models},
    journaltitle = {Programming and Computer Software},
    date = {2023},
    volume = {49},
    number = {7},
    pages = {559--565},
    doi = {10.1134/S0361768823070034},
    issn = {0361-7688},
    publisher = {Pleiades Publishing}
}

2021

Runtime Verification of Operating Systems Based on Abstract Models (Russian)
Efremov D.V., Kopach V.V., Kornykhin E.V., Kuliamin V.V., Petrenko A.K., Khoroshilov A.V., Shchepetkov I.V. Proceedings of ISP RAS, Vol. 33, No. 6, pp. 15–26 · DOI · PDF

BibTeXBibLaTeX

@article{efremov_rv_isp_2021,
    author = {Efremov, D. V. and Kopach, V. V. and Kornykhin, E. V. and Kuliamin, V. V. and Petrenko, A. K. and Khoroshilov, A. V. and Shchepetkov, I. V.},
    title = {Runtime Verification of Operating Systems Based on Abstract Models},
    journal = {Proceedings of the Institute for System Programming of the RAS},
    year = {2021},
    volume = {33},
    number = {6},
    pages = {15--26},
    doi = {10.15514/ISPRAS-2021-33(6)-2},
    issn = {2079-8156},
    publisher = {Institute for System Programming of the Russian Academy of Sciences},
    url = {https://ispranproceedings.elpub.ru/jour/article/view/1469}
}

@article{efremov_rv_isp_2021,
    author = {Efremov, D. V. and Kopach, V. V. and Kornykhin, E. V. and Kuliamin, V. V. and Petrenko, A. K. and Khoroshilov, A. V. and Shchepetkov, I. V.},
    title = {Runtime Verification of Operating Systems Based on Abstract Models},
    journaltitle = {Proceedings of the Institute for System Programming of the RAS},
    date = {2021},
    volume = {33},
    number = {6},
    pages = {15--26},
    doi = {10.15514/ISPRAS-2021-33(6)-2},
    issn = {2079-8156},
    publisher = {Institute for System Programming of the Russian Academy of Sciences},
    url = {https://ispranproceedings.elpub.ru/jour/article/view/1469}
}

2020

Monitoring and Testing Based on Multi-Level Program Specifications (Russian)
Petrenko A.K., Efremov D.V., Kornykhin E.V., Kuliamin V.V., Khoroshilov A.V., Shchepetkov I.V. Proceedings of ISP RAS, Vol. 32, No. 6, pp. 7–18 · DOI · PDF

BibTeXBibLaTeX

@article{petrenko_multilevel_specs_2020,
    author = {Petrenko, A. K. and Efremov, D. V. and Kornykhin, E. V. and Kuliamin, V. V. and Khoroshilov, A. V. and Shchepetkov, I. V.},
    title = {Monitoring and Testing Based on Multi-Level Program Specifications},
    journal = {Proceedings of the Institute for System Programming of the RAS},
    year = {2020},
    volume = {32},
    number = {6},
    pages = {7--18},
    doi = {10.15514/ISPRAS-2020-32(6)-1},
    issn = {2079-8156},
    url = {https://ispranproceedings.elpub.ru/jour/article/view/1357}
}

@article{petrenko_multilevel_specs_2020,
    author = {Petrenko, A. K. and Efremov, D. V. and Kornykhin, E. V. and Kuliamin, V. V. and Khoroshilov, A. V. and Shchepetkov, I. V.},
    title = {Monitoring and Testing Based on Multi-Level Program Specifications},
    journaltitle = {Proceedings of the Institute for System Programming of the RAS},
    date = {2020},
    volume = {32},
    number = {6},
    pages = {7--18},
    doi = {10.15514/ISPRAS-2020-32(6)-1},
    issn = {2079-8156},
    url = {https://ispranproceedings.elpub.ru/jour/article/view/1357}
}

Runtime Verification of Linux Kernel Security Module
Efremov Denis, Shchepetkov Ilya FM 2019 International Workshops, LNCS 12233, pp. 185–199, Springer · DOI · arXiv · PDF

BibTeXBibLaTeX

@inproceedings{efremov_rv_lsm_fm2019,
    author = {Efremov, Denis and Shchepetkov, Ilya},
    editor = {Sekerinski, Emil and Moreira, Nelma and Oliveira, Jos{\'e} N. and Ratiu, Daniel and et al.},
    title = {Runtime Verification of Linux Kernel Security Module},
    booktitle = {Formal Methods. FM 2019 International Workshops},
    series = {Lecture Notes in Computer Science},
    volume = {12233},
    year = {2020},
    publisher = {Springer International Publishing},
    address = {Cham},
    pages = {185--199},
    doi = {10.1007/978-3-030-54997-8_12},
    isbn = {978-3-030-54997-8},
    issn = {0302-9743},
    url = {https://link.springer.com/chapter/10.1007/978-3-030-54997-8_12},
    eprint = {2001.01442},
    archiveprefix = {arXiv}
}

@inproceedings{efremov_rv_lsm_fm2019,
    author = {Efremov, Denis and Shchepetkov, Ilya},
    editor = {Sekerinski, Emil and Moreira, Nelma and Oliveira, Jos{\'e} N. and Ratiu, Daniel and et al.},
    title = {Runtime Verification of Linux Kernel Security Module},
    booktitle = {Formal Methods. FM 2019 International Workshops},
    series = {Lecture Notes in Computer Science},
    volume = {12233},
    date = {2020},
    publisher = {Springer International Publishing},
    location = {Cham},
    pages = {185--199},
    doi = {10.1007/978-3-030-54997-8_12},
    isbn = {978-3-030-54997-8},
    issn = {0302-9743},
    url = {https://link.springer.com/chapter/10.1007/978-3-030-54997-8_12},
    eprint = {2001.01442},
    eprinttype = {arxiv}
}

2019

Modeling and Verification of Access Control Security Policies in Operating Systems (Russian)
Devyanin P.N., Efremov D.V., Kuliamin V.V., Petrenko A.K., Khoroshilov A.V., Shchepetkov I.V. Book · Goryachaya Liniya – Telekom, Moscow, 214 pp. · ISBN 978-5-9912-0787-4 · PDF

BibTeXBibLaTeX

@book{devyanin_security_monograph_2019,
    author = {Devyanin, P. N. and Efremov, D. V. and Kuliamin, V. V. and Petrenko, A. K. and Khoroshilov, A. V. and Shchepetkov, I. V.},
    title = {Modeling and Verification of Access Control Security Policies in Operating Systems},
    publisher = {Goryachaya Liniya -- Telekom},
    year = {2019},
    address = {Moscow, Russian Federation},
    pages = {214},
    isbn = {978-5-9912-0787-4},
    url = {http://www.ispras.ru/publications/2018/security_policy_modeling_and_verification/}
}

@book{devyanin_security_monograph_2019,
    author = {Devyanin, P. N. and Efremov, D. V. and Kuliamin, V. V. and Petrenko, A. K. and Khoroshilov, A. V. and Shchepetkov, I. V.},
    title = {Modeling and Verification of Access Control Security Policies in Operating Systems},
    publisher = {Goryachaya Liniya -- Telekom},
    date = {2019},
    location = {Moscow, Russian Federation},
    pagetotal = {214},
    isbn = {978-5-9912-0787-4},
    url = {http://www.ispras.ru/publications/2018/security_policy_modeling_and_verification/}
}

ACSL by Example: Towards a Formally Verified Standard Library
Gerlach Jens, Efremov Denis, Sikatzki Tim et al. Technical Report v19.0.0 · Fraunhofer FOKUS · PDF

BibTeXBibLaTeX

@article{acsl_by_example_2019,
    author = {Gerlach, Jens and Efremov, Denis and Sikatzki, Tim and others},
    title = {{ACSL by Example}: Towards a Formally Verified Standard Library},
    journal = {Fraunhofer {FOKUS} Technical Report},
    year = {2019},
    edition = {19.0.0},
    month = jun,
    url = {https://github.com/fraunhoferfokus/acsl-by-example/raw/master/ACSL-by-Example.pdf}
}

@report{acsl_by_example_2019,
    author = {Gerlach, Jens and Efremov, Denis and Sikatzki, Tim and others},
    title = {{ACSL by Example}: Towards a Formally Verified Standard Library},
    type = {Technical Report},
    institution = {Fraunhofer {FOKUS}},
    date = {2019-06},
    version = {19.0.0},
    url = {https://github.com/fraunhoferfokus/acsl-by-example/raw/master/ACSL-by-Example.pdf}
}

2018

Deductive Verification of Unmodified Linux Kernel Library Functions
Efremov Denis, Mandrykin Mikhail, Khoroshilov Alexey ISoLA 2018, LNCS 11245, pp. 216–234, Springer · DOI · arXiv · PDF

BibTeXBibLaTeX

@inproceedings{efremov_verker_isola_2018,
    author = {Efremov, Denis and Mandrykin, Mikhail and Khoroshilov, Alexey},
    editor = {Margaria, Tiziana and Steffen, Bernhard},
    title = {Deductive Verification of Unmodified Linux Kernel Library Functions},
    booktitle = {Leveraging Applications of Formal Methods, Verification and Validation. Verification},
    series = {Lecture Notes in Computer Science},
    volume = {11245},
    year = {2018},
    publisher = {Springer International Publishing},
    address = {Cham},
    pages = {216--234},
    doi = {10.1007/978-3-030-03421-4_15},
    isbn = {978-3-030-03421-4},
    issn = {0302-9743},
    url = {https://link.springer.com/chapter/10.1007/978-3-030-03421-4_15},
    eprint = {1809.00626},
    archiveprefix = {arXiv}
}

@inproceedings{efremov_verker_isola_2018,
    author = {Efremov, Denis and Mandrykin, Mikhail and Khoroshilov, Alexey},
    editor = {Margaria, Tiziana and Steffen, Bernhard},
    title = {Deductive Verification of Unmodified Linux Kernel Library Functions},
    booktitle = {Leveraging Applications of Formal Methods, Verification and Validation. Verification},
    series = {Lecture Notes in Computer Science},
    volume = {11245},
    date = {2018},
    publisher = {Springer International Publishing},
    location = {Cham},
    pages = {216--234},
    doi = {10.1007/978-3-030-03421-4_15},
    isbn = {978-3-030-03421-4},
    issn = {0302-9743},
    url = {https://link.springer.com/chapter/10.1007/978-3-030-03421-4_15},
    eprint = {1809.00626},
    eprinttype = {arxiv}
}

Lemma Functions for Frama-C: C Programs as Proofs
Volkov Grigoriy, Mandrykin Mikhail, Efremov Denis ISPRAS Open 2018, pp. 31–38, IEEE · DOI · arXiv · PDF

BibTeXBibLaTeX

@inproceedings{volkov_lemma_functions_2018,
    author = {Volkov, Grigoriy and Mandrykin, Mikhail and Efremov, Denis},
    title = {Lemma Functions for {Frama-C}: {C} Programs as Proofs},
    booktitle = {Proceedings of the 2018 Ivannikov ISPRAS Open Conference (ISPRAS-2018)},
    year = {2018},
    pages = {31--38},
    doi = {10.1109/ISPRAS.2018.00012},
    isbn = {978-1-7281-1275-6},
    publisher = {IEEE},
    url = {https://ieeexplore.ieee.org/document/8675145},
    eprint = {1811.05879},
    archiveprefix = {arXiv}
}

@inproceedings{volkov_lemma_functions_2018,
    author = {Volkov, Grigoriy and Mandrykin, Mikhail and Efremov, Denis},
    title = {Lemma Functions for {Frama-C}: {C} Programs as Proofs},
    booktitle = {Proceedings of the 2018 Ivannikov ISPRAS Open Conference (ISPRAS-2018)},
    date = {2018},
    pages = {31--38},
    doi = {10.1109/ISPRAS.2018.00012},
    isbn = {978-1-7281-1275-6},
    publisher = {IEEE},
    url = {https://ieeexplore.ieee.org/document/8675145},
    eprint = {1811.05879},
    eprinttype = {arxiv}
}

2017

Formal Verification of Linux Kernel Library Functions (Russian)
Efremov Denis, Mandrykin Mikhail Proceedings of ISP RAS, Vol. 29, No. 6, pp. 49–76 · DOI · PDF

BibTeXBibLaTeX

@article{efremov_verker_ispras_2017,
    author = {Efremov, Denis and Mandrykin, Mikhail},
    title = {Formal Verification of Linux Kernel Library Functions},
    journal = {Proceedings of the Institute for System Programming of the RAS},
    year = {2017},
    volume = {29},
    number = {6},
    pages = {49--76},
    doi = {10.15514/ISPRAS-2017-29(6)-3},
    issn = {2079-8156},
    url = {https://ispranproceedings.elpub.ru/jour/article/view/418}
}

@article{efremov_verker_ispras_2017,
    author = {Efremov, Denis and Mandrykin, Mikhail},
    title = {Formal Verification of Linux Kernel Library Functions},
    journaltitle = {Proceedings of the Institute for System Programming of the RAS},
    date = {2017},
    volume = {29},
    number = {6},
    pages = {49--76},
    doi = {10.15514/ISPRAS-2017-29(6)-3},
    issn = {2079-8156},
    url = {https://ispranproceedings.elpub.ru/jour/article/view/418}
}

2015

Construction of the Operating System Kernel (Russian)
Efremov D.V., Komarov N.Yu., Khoroshilov A.V. Textbook · MSU/MAKS Press, Moscow, 160 pp. · ISBN 978-5-89407-549-5 · PDF

BibTeXBibLaTeX

@book{efremov_osdev_book_2015,
    author = {Efremov, D. V. and Komarov, N. Yu. and Khoroshilov, A. V.},
    title = {Construction of the Operating System Kernel},
    publisher = {Publishing Department of the CMC Faculty of Lomonosov Moscow State University; MAKS Press},
    year = {2015},
    address = {Moscow},
    pages = {160},
    isbn = {978-5-89407-549-5},
    url = {https://www.elibrary.ru/item.asp?id=25670418}
}

@book{efremov_osdev_book_2015,
    author = {Efremov, D. V. and Komarov, N. Yu. and Khoroshilov, A. V.},
    title = {Construction of the Operating System Kernel},
    publisher = {Publishing Department of the CMC Faculty of Lomonosov Moscow State University; MAKS Press},
    date = {2015},
    location = {Moscow},
    pagetotal = {160},
    isbn = {978-5-89407-549-5},
    url = {https://www.elibrary.ru/item.asp?id=25670418}
}

2014

Tools Support for Linux Kernel Deductive Verification Workflow
Efremov Denis, Komarov Nikita SYRCoSE 2014, Vol. 8, No. 6, pp. 39–44 · DOI · PDF

BibTeXBibLaTeX

@inproceedings{efremov_verif_tools_2014,
    author = {Efremov, Denis and Komarov, Nikita},
    title = {Tools Support for Linux Kernel Deductive Verification Workflow},
    booktitle = {Proceedings of the Spring/Summer Young Researchers' Colloquium on Software Engineering (SYRCoSE)},
    year = {2014},
    volume = {8},
    number = {6},
    pages = {39--44},
    doi = {10.15514/SYRCOSE-2014-8-6},
    issn = {2311-7230},
    url = {https://cyberleninka.ru/article/n/tools-support-for-linux-kernel-deductive-verification-workflow},
    address = {Saint Petersburg, Russia}
}

@inproceedings{efremov_verif_tools_2014,
    author = {Efremov, Denis and Komarov, Nikita},
    title = {Tools Support for Linux Kernel Deductive Verification Workflow},
    booktitle = {Proceedings of the Spring/Summer Young Researchers' Colloquium on Software Engineering (SYRCoSE)},
    date = {2014},
    volume = {8},
    number = {6},
    pages = {39--44},
    doi = {10.15514/SYRCOSE-2014-8-6},
    issn = {2311-7230},
    url = {https://cyberleninka.ru/article/n/tools-support-for-linux-kernel-deductive-verification-workflow},
    location = {Saint Petersburg, Russia}
}

2012

Sevigator: Network Confinement of Malware Applications and Untrusted Operating Systems
Efremov Denis, Pakulin Nikolay SECRYPT 2012, pp. 395–398, SciTePress · DOI · PDF

BibTeXBibLaTeX

@inproceedings{efremov_sevigator_2012,
    author = {Efremov, Denis and Pakulin, Nikolay},
    title = {Sevigator: Network Confinement of Malware Applications and Untrusted Operating Systems},
    booktitle = {Proceedings of the International Conference on Security and Cryptography (SECRYPT 2012)},
    year = {2012},
    pages = {395--398},
    isbn = {978-989-8565-24-2},
    doi = {10.5220/0004095103950398},
    publisher = {SciTePress},
    address = {Rome, Italy},
    url = {https://www.researchgate.net/publication/233968192_Sevigator_Network_Confinement_of_Malware_Applications_and_Untrusted_Operating_Systems}
}

@inproceedings{efremov_sevigator_2012,
    author = {Efremov, Denis and Pakulin, Nikolay},
    title = {Sevigator: Network Confinement of Malware Applications and Untrusted Operating Systems},
    booktitle = {Proceedings of the International Conference on Security and Cryptography (SECRYPT 2012)},
    date = {2012},
    pages = {395--398},
    isbn = {978-989-8565-24-2},
    doi = {10.5220/0004095103950398},
    publisher = {SciTePress},
    location = {Rome, Italy},
    url = {https://www.researchgate.net/publication/233968192_Sevigator_Network_Confinement_of_Malware_Applications_and_Untrusted_Operating_Systems}
}

2011

Protection of the Applications' Privacy Running Untrusted Operating System (Russian)
Efremov Denis APSSE 2011 · PDF

BibTeXBibLaTeX

@inproceedings{efremov_hypervisor_2011,
    author = {Efremov, Denis},
    title = {Protection of the Applications' Privacy Running Untrusted Operating System},
    booktitle = {Proceedings of the Russian Conference on Actual Problems of System and Software Engineering (APSSE)},
    year = {2011}
}

@inproceedings{efremov_hypervisor_2011,
    author = {Efremov, Denis},
    title = {Protection of the Applications' Privacy Running Untrusted Operating System},
    booktitle = {Proceedings of the Russian Conference on Actual Problems of System and Software Engineering (APSSE)},
    date = {2011}
}

2010

An Approach to On-the-Fly Activation and Deactivation of Virtualization-Based Security Systems
Efremov Denis, Iakovenko Pavel SYRCoSE 2010, Vol. 4, pp. 157–161 · DOI · PDF

BibTeXBibLaTeX

@inproceedings{efremov_sec_activation_2010,
    author = {Efremov, Denis and Iakovenko, Pavel},
    title = {An Approach to On-the-Fly Activation and Deactivation of Virtualization-Based Security Systems},
    booktitle = {Proceedings of the Spring/Summer Young Researchers' Colloquium on Software Engineering (SYRCoSE)},
    year = {2010},
    volume = {4},
    pages = {157--161},
    doi = {10.15514/SYRCOSE-2010-4-31},
    issn = {2311-7230},
    url = {https://cyberleninka.ru/article/n/an-approach-to-on-the-fly-activation-and-deactivation-of-virtualization-based-security-systems},
    address = {Nizhny Novgorod, Russia}
}

@inproceedings{efremov_sec_activation_2010,
    author = {Efremov, Denis and Iakovenko, Pavel},
    title = {An Approach to On-the-Fly Activation and Deactivation of Virtualization-Based Security Systems},
    booktitle = {Proceedings of the Spring/Summer Young Researchers' Colloquium on Software Engineering (SYRCoSE)},
    date = {2010},
    volume = {4},
    pages = {157--161},
    doi = {10.15514/SYRCOSE-2010-4-31},
    issn = {2311-7230},
    url = {https://cyberleninka.ru/article/n/an-approach-to-on-the-fly-activation-and-deactivation-of-virtualization-based-security-systems},
    location = {Nizhny Novgorod, Russia}
}

Software Registrations (3)

CVEhound — State Registration No. RU 2021663474 (Aug 2021) · FIPS

System Call Replay on Event-B Models — Registration No. RU 2020661855 (Oct 2020) · FIPS

C Source Code Transformation for Subsequent Verification — Registration No. RU 2015617942 (Jul 2015) · FIPS

Projects

Own Projects

Floppy driver maintainer since Jul 2019
Coccinelle 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
modpost check for static EXPORT_SYMBOL* functions (commit)
Full commit list

Syzkaller

Driver fuzzing rules: integrity (IMA/EVM), smack, floppy, cdrom, i2c
Full list of PRs

Gentoo

Portage ebuilds

Other Contributions

kernel-hardening-checker — security hardening config checker
Kaitai Struct — binary format definitions
Contiki NG — IoT operating system
Opam — OCaml package repository

Talks

CVEhound: Audit Kernel Sources for Missing CVE Fixes Linux Security Summit 2021

Video Slides

CVEhound: проверка исходников Linux на известные CVE ZeroNights 2021

Video Slides

Формальная верификация ядер операционных систем PHDays X 2021

Video Slides

Инструменты тестирования ядра Linux OSSDEVCONF 2021

Video Slides

Continuous Deductive Verification with Frama-C FCSD 2019

Runtime Verification of Linux Kernel Security Module FM 2019 Workshop

Deductive Verification of Unmodified Linux Kernel Library Functions ISoLA 2018, Limassol

Slides

Практический язык извлечения данных из исходных кодов и их подготовки к анализу Yandex Perl Meetup 2018

Video

Формальная верификация кода на языке C PHDays VII 2017

Video Slides

Security Policy Modeling and Verification (part 3) ISPRAS Open 2017

Teaching

Construction of the Operating System Kernel (Russian) — MSU (Spring 2013, Fall 2014–2018), HSE (Fall 2016–2018), MIPT (Fall 2015–2018)
Software Verification (Russian) — HSE (Spring 2016–2017)

Denis Efremov

Experience

Education

Skills

Publications

2025

2023

2021

2020

2019

2018

2017

2015

2014

2012

2011

2010

Projects

CVEhound

CruelKernel

adb_root

VerKer

Spec-Utils

lsm_bpf_check_argc0

Talks

Teaching