Publications in English

2019
Nikita Malyshev, Irina Dudina, Daniil Kutz, Alexander Novikov, Sergey Vartanov
SMT Solvers in Application to Static and Dynamic Symbolic Execution: A Case Study
2019 Ivannikov Ispras Open Conference (ISPRAS), Moscow, Russia, 2019, pp. 9-15.
Keywords: symbolic execution, static analysis, SMT solvers, QF_BV, solver portfolio

This paper studies the performance and working aspects of SMT solvers on processing formulas acquired during path-sensitive static analysis and dynamic symbo...

2018
Andrey Belevantsev, Alexey Borodin, Irina Dudina, Valery Ignatiev, Alexey Izbyshev, Sergey Polyakov, Evgeny Velesevich, Dmitry Zhurikhin
Design and Development of Svace Static Analyzers
Ivannikov Memorial Workshop, IEEE Computer Society Conference Publishing Services Yerevan, Armeniya, pp 3-9

Static analysis became the mainstream technology that is widely used in secure development lifecycles. As such it is covered by a lot of research works highl...

2018
I.A. Dudina
Buffer Overflow Detection via Static Analysis: Expectations vs. Reality
Proceedings of the Institute for System Programming, vol. 30, issue 3, pp. 21-30.
Keywords: software error detection; static analysis; buffer overrun

Over the last few decades buffer overflow remains one of the main sources of program errors and vulnerabilities. Among other solutions several static analysi...

2017
Dudina, I. A. and Belevantsev, A. A.
Using Static Symbolic Execution to Detect Buffer Overflows
Programming and Computer Software, Volume 43, Issue 5, pp 277–288
Keywords: Buffer overflow, static symbolic execution

Buffer overrun remains one of the main sources of errors and vulnerabilities in the C/C++ source code. To detect such kind of defects, static analysis is wid...

2015
Koshelev V.K., Dudina I.A., Izbyshev A.O.
Interprocedural Taint Analysis for LLVM-bitcode
Programming and Computer Software, Volume 41, Issue 4, pp 237–245

In the paper, taint analysis problem is considered. To solve it, static interprocedural context-, flow-, and object-sensitive algorithm is proposed. Characte...