|
|
 |
 |
 |
Захаров Владимир Анатольевич
доцент
электронный адрес: zakh@cs.msu.su
телефон (раб.): (095) 939 1772
факс: (095) 939 2596
области научных интересов
-
Для формальных моделей последовательных, рекурсивных и параллельных программ исследуется
проблема эквивалентности: верно ли, что две заданные произвольные программы имеют одинаковое
поведение. Решение этой задачи находит применение при разработке оптимизирующих преобразований
программ, при проведении реорганизации (рефакторинга) программ, при проектировании СБИС,
при разработке антивирусных сканеров, при проверке стойкости криптографических протоколов.
публикации
- Захаров В.А. Формальные модели программ и свободные схемы
Программирование, 1992, N 2, с.10-24
- Захаров В.А. Об одном критерии сравнимости операторных формальных моделей программ
Программирование, 1993, N 4, с.12-25
- Захаров В.А. О свободных схемах в формальных моделях программ
Математические вопросы кибернетики, 1994, вып. 5, с.208-239
- Захаров В.А. Условия сглаживаемости операторных формальных моделей программ
Программирование, 1994, N 5, с.23-40
- Захаров В.А. Об отношении аппроксимируемости семантик операторных программ
Вестник Московского университета, сер. 15, Вычислительная математика и
кибернетика, 1994, N 4, с.54-60
- Захаров В.А. Полиномиальный алгоритм разрешения проблемы эквивалентности унарных линейных
рекурсивных схем программ
(ps)
Сборник трудов II Международной конференции "Дискретные модели в теории
управляющих систем", Красновидово-97, с.26-29
- Захаров В.А. О проблеме эквивалентности операторных схем на упорядоченных полугрупповых
моделях
(ps)
Сборник трудов III Международной конференции "Дискретные модели в теории
управляющих систем", Красновидово-98, с.36-40
- Подловченко Р.И., Захаров В.А. Полиномиальный по сложности алгоритм, распознающий коммутативную эквивалентность
схем программ
(ps)
Доклады РАН, 1998, т. 362, N 6 (совм. с Р.И.Подловченко)
- Zakharov V.A. An Efficient and Unified Approac to the Decidability of Equivalence of
Propositional Program Schemes
(ps)
Lecture Notes in Computer Science, Springer-Verlag, 1998,
v.1443, p.247-259.
- Захаров В.А. Быстрые алгоритмы разрешения эквивалентности операторных программ
на упорядоченных шкалах
(ps)
Математические вопросы кибернетики, 1998, вып. 7, с.303-324
- Захаров В.А. Аппроксимация абстрактных семантик формальными моделями программ
Дискретная математика, 1998, том 10, вып. 4, с.119-141
- Захаров В.А. Об эффективной разрешимости проблемы эквивалентности линейных унарных
рекурсивных программ
(ps)
Математические вопросы кибернетики, 1999, вып. 8, с.255-273
- Захаров В.А. Быстрые алгоритмы разрешения эквивалентности пропозициональных операторных
программ на упорядоченных полугрупповых шкалах
(ps)
Вестник Московского университета, сер. 15, Вычислительная математика и
кибернетика, 1999, N 3, с.29-35
- Захаров В.А. О разрешимости проблемы эквивалентности в одном классе операторных
программ
(ps)
Сборник "Прикладная математика и информатика", Изд-во ВМиК МГУ, 1999, вып. 5
с.99-100
- Zakharov V.A. On the decidability of the equivalence problem for orthogonal sequential
programs
(ps)
Grammars, Kluer Academic Publishers, 1999, v.2, N 3, p.271-281
- Захаров В.А. Общие методы построения разрешающих алгоритмов для проблемы эквивалентности
пропозициональных операторных программ
(ps)
Сборник трудов IV Международной конференции "Дискретные модели в теории
управляющих систем", Красновидово-00, с.25-29
- Захаров В.А., К.А.Соколова. О разрешимости проблемы эквивалентности в одном классе металинейных
унарных рекурсивных программ
(ps)
Сборник трудов IV Международной конференции "Дискретные модели в теории
управляющих систем", Красновидово-00, с.29-31
- Захаров В.А. О проблеме эквивалентности для схем программ с операторами засылки констант
(ps)
Сборник трудов IV Международной конференции "Дискретные модели в теории
управляющих систем", Красновидово-00, с.153-154
- Zakharov V.A. On the Decidability of the Equivalence Problem for Monadic Recursive Programs
(ps)
Theoretical Information and Applications, 2000, v.34, N 2, p.157-171
- Zakharov V.A. On the approximation relation on dynamic logic models.
Abstracts of contributed papers, Logic Colloquium 2000, Paris, La Sorbonne,
23-31 juillet 2000
- Zakharov V.A. The equivalence problem for computational models: Decidable and Undecidable Cases
Proc. of Int. Conf. "Models of Universal Computations",
Lecture Notes in Computer Science, Vol. 2055, 2001, p.133-153
- Захаров В.А. О проблеме эквивалентности операторных программ на одном классе уравновешенных шкал.
Материалы VII Международного семинара "Дискретная математика и ее приложения",
Изд-во механико-математического ф-та МГУ, 2001, с. 54-57
- Захаров В.А. О проблеме эквивалентности операторных программ на уравновешенных однородных обратимых шкалах.
Математические вопросы кибернетики, Физматлит, 2001, вып.10.
- Захаров В.А., Захарьящев И.М. Об одной полисемантической модели последовательных программ.
Труды V Международной конференции "Дискретные модели в теории управляющих систем", (Ратмино, 26-29 мая 2003 г.), с. 33-34.
- Zakharov V.A., Zakharyaschev I.M. An equivalence-checking algorithm for polysemantic models of sequential programs.
Proceedings of the International Workshop on Program Understanding (14-16 July, Altai Mountains, Russia), 2003,
p. 59-70.
- Захаров В.А. Об одной алгебраической модели программ, связанной с обработкой прерываний.
Материалы VIII Международного семинара "Дискретная математика и ее приложения",
Изд-во механико-математического ф-та МГУ, 2004, с. 129-131.
- Захаров В.А., Захарьящев И.М. О сложности проблемы эквивалентности в модели программ с перестановочными и монотонными операторами.
Материалы VIII Международного семинара "Дискретная математика и ее приложения",
Изд-во механико-математического ф-та МГУ, 2004, с. 131-134.
- Zakharov V.A., Zakharyaschev I.M. On the equivalence-checking problem for a model of programs related with multi-tape automata.
Proceedings of CIAA-2004 "The 9-th International Conference on Implementation and Application of Automata"
(July 22-24, 2004), Kingston, Ontario, Canada, Lecture Notes in Computer Science, v. 3317, 2005, p. 293-305, p. 59-70.
- Zakharov V.A., Zakharyaschev I.M. On the equivalence-checking problem for polysemantic models of sequential programs.
Труды Института Системного программирования: Том 6. (под Ред. В.П Иванникова) - М.:ИСП РАН., 2004, с. 182-199.
- Захаров В.А., Иванов К.С. Об одной модели последовательных программ с динамической памятью.
Труды 6-ой Международной конференции "Дискретные модели в теории управляющих систем", (7-11 декабря 2004 г., Москва),
2004, c.112-116.
- Захаров В.А., Захарьящев И.М. О проблеме эквивалентности для программ с частично перестановочными и монотонными операторами.
Труды 6-ой Международной конференции "Дискретные модели в теории управляющих систем", (7-11 декабря 2004 г., Москва),
2004, c.105-110.
- Zakharov V.A., Zakharyaschev I.M. On the equivalence-checking problem for sequential programs with partially commuting and monotonic statements.
Proceedings of the XI Congress of Mathematics of Serbia and Montenegro (September 28-October 2, 2004), Petrovac,
Montenegro, 2004, p. 79.
- Захаров В.А., Подловченко Р.И. Проверка эквивалентности программ: модели и алгоритмы.
Тезисы докладов XIV Международной конференции "Проблемы теоретической кибернетики", Пенза, 23-28 мая, 2005.
- Захаров В.А., Подловченко Р.И., И.М. Захарьящев, Д.М. Русаков, В.Л. Щербина. О возможности применения быстрых алгоритмов проверки эквивалентности программ для обнаружения вирусов.
Труды 2-ой Всероссийской научной конференции "Методы и средства обработки информации", Москва, 2005, с. 414-421.
- Podlovchenko R.I., Rusakov D. M., Zakharov V.A. On the equivalence problem for programs with mode switching.
Proceedings of CIAA-2005 "The 10-th International Conference on Implementation and Application of Automata" (June 27-29, 2005), Sophia Antipolis, France, Lecture Notes in Computer Science, v. 3317, 2006, v. 3845, p. 351-352.
- Захаров В.А., Щербина В.Л. О сложности распознавания эквивалентности машин Тьюринга без записи на ленту.
Материалы XIV международной школы-семинара "Синтез и сложность управляющих систем" (Санкт-Петербург, 26-30 июня 2006 г.),
2006, с. 147-150.
- Захаров В.А., Иванов К.С. О проблеме логико-термальной эквивалентности последовательных программ с динамической памятью.
Труды Института Системного программирования: Том 11. (под Ред. В.П Иванникова) - М.:ИСП РАН, 2006, с. 61-82.
- Podlovchenko R.I., Rusakov D. M., Zakharov V.A. The equivalence problem for programs with mode switching is PSPACE-complete.
Труды Института Системного программирования: Том 11. (под Ред. В.П Иванникова) - М.:ИСП РАН, 2006, с. 111-135.
- Захаров В.А., Щербина В.Л. Об эквивалентности программ с операторами, обладающими свойствами коммутативности и подавления.
Материалы 9-го Международного семинара "Дискретная математика и ее приложения", Москва, 2007, c. 191-194.
- Захаров В.А., Щербина В.Л. Эффективные алгоритмы проверки эквивалентности программ в моделях, связанных с обработкой прерываний.
Вестник Московского университета, Серия Вычислительная математика и кибернетика, 2008, N 2, с. 33-41.
- Захаров В.А. О проблеме эквивалентности в одном классе монадических линейных программ.
Тезисы докладов 15-ой международной конференции "Проблемы теоретической кибернетики" (Казань, 2-7 июня, 2008 г.)
- Захаров В.А., Щербина В.Л. О сложности проверки эквивалентности программ с операторами засылки констант.
Труды 8-ой Международной конференции "Дискретные модели в теории управляющих систем", Москва, 6-9 апреля 2009 г., 2009, с. 369-374.
-
Обфускация - это такая разновидность преобразований программ, которая сохраняет функциональные характеристики
программ, но препятствует извлечению из открытого текста преобразованной программы полезной информации
об устройстве ее алгоритма, структур данных, секретных ключей и пр. Основные задачи в этой области криптографии - разработка
обфускирующих преобразований программ и оценка их стойкости.
публикации
- Zakharov V.A. To the obfuscation of sequential program control-flow
Труды XII Байкальской международной конференции, Иркутск, Байкал, 24-июня-1 июля 2001 г., т.5, 2001, с. 57-61.
- Chow S., Gu Y., Johnson H., Zakharov V.A. An approach to the obfuscation of control-flow of sequential computer programs.
Proc. of Information Security Confernce, Lecture Notes in Computer Science, Vol. 2200, 2001, p.144-155.
- Захаров В.А., Варновский Н.П. К вопросу о существовании стойких обфускаторов программ.
Труды V Международной конференции "Дискретные модели в теории управляющих систем", (Ратмино, 26-29 мая 2003 г.), с.17-19.
- Varnovsky N.P., Zakharov V.A. On the possibility of provably secure obfuscating programs.
Proceedings of the Andrei Ershov 5th International Conference "Prespectives of System Informatics" (9-12 July 2003, Novosibirsk),
Lecture Notes in Computer Science, v. 2890, 2003, p. 91-102.
- Варновский Н.П., Захаров В.А., Кузюрин Н.П., Шокуров А.В. О перспективах решения задачи обфускации компьютерных программ.
Верификация распределенных программ в системе имитационного моделирования DYANA.
Труды конференции (МаБИТ-03) (Москва, 22-24 октября 2003 г.), 2004, c. 344-352.
- Захаров В.А., Иванов К.С. О противодействии некоторым алгоритмам статического анализа программ.
Труды конференции (МаБИТ-03) (Москва, 22-24 октября 2003 г.), 2004, c. 282-287.
- Zakharov V.A., Ivanov K.S. Program obfuscation as obstruction of program static analysis.
Труды Института Системного программирования: Том 6. (под Ред. В.П Иванникова) - М.:ИСП РАН., 2004, с. 141-161.
- Варновский Н.П., Захаров В.А., Кузюрин Н.П. Математические проблемы обфускации
Труды конференции "Математика и безопасность информационных технологий" (МаБИТ-04) (Москва, 28-29 октября 2004 г.), 2005 г.
- Н.П. Варновский, Захаров В.А., В.П. Иванников, Н.Н. Кузюрин, А.В. Шокуров, А.Н. Кононов, А.В. Калинин. Методы защиты проектных
решений при проектировании микроэлектронных схем
Известия ТРТУ, Таганрог, Изд-во ТРГУ, N 4, 2005, с. 112-119.
- Варновский Н.П., Захаров В.А., Кузюрин Н.П., Шокуров А.В. К вопросу об обфускации конечных автоматов.
Материалы IX международной конференции "Интеллектуальные системы и компьютерные науки" (23-27 октября 2006 г.), т. 1, Часть 1,
2006, с. 127-130.
- Варновский Н.П., Захаров В.А., Кузюрин Н.П., Шокуров А.В. О проблеме обфускации программ.
Материалы зимних научных чтений факультета социологии и информационных технологий и
XIII социологических чтений Российского государственного социального университета (1-4 февраля 2006 года), 2008. С. 204-206.
- Варновский Н.П., Захаров В.А., Кузюрин Н.П., Шокуров А.В., Чернов А.В.
Об особенностях применения методов обфускации программ для информационной защиты микроэлектронных схем.
Труды Института Системного программирования: Том 11. (под Ред. В.П Иванникова) - М.:ИСП РАН, 2006, с. 29-60.
- Kuzurin N.N., Shokurov A.V., Varnovsky N.P., Zakharov V.A. Using algebraic models of programs for detecting metamorphic malwares.
Труды Института Системного программирования: Том 12. (под Ред. В.П Иванникова) - М.:ИСП РАН, 2007, с. 77-94.
- Варновский Н.П. , Захаров В.А., Кузюрин Н.Н., Шокуров А.В. Современные методы обфускации программ: классификация и сравнительный анализ.
Известия ЮФУ, 2007, N 1.
- Kuzurin N.N., Shokurov A.V., Varnovsky N.P., Zakharov V.A. On the concept of software obfuscation in computer security.
Proc. of Information Security Confernce, Lecture Notes in Computer Science, 2007, p. 281-298.
- Варновский Н.П. , Захаров В.А., Кузюрин Н.Н., Шокуров А.В. О стойкой обфускации компьютерных программ.
Научные ведомости Белгородского государственного университета, Серия История. Политология. Экономика. Информатика. 2009,
N 15, Вып. 12/1, с. 97-105.
-
Задача верификации моделей программ (model checking) состоит в том, чтобы для заданной модели программ,
представленной системой переходов, выражением алгебры процессов,
автоматом и пр., и спецификации программы, представленной формулой темпоральной логики, требуется
проверки выполнимость спецификации на модели.
публикации
- Zakharov V.A. On the verification of PLTL formulae by means of monotone disjunctive
normal forms
(ps)
Lecture Notes in Computer Science, Springer-Verlag, 1997,
v.1234, p.419-429
- Захаров В.А., Царьков Д.В. Эффективные алгоритмы проверки выполнимости формул
темпоральной логики CTL и их применение для верификации параллельных программ
(ps)
Программирование, 1998, N 4
- Bakhmurov F.G., Chistolinov M.V., Smelyansky R.L., Vinter K., Ypatko I.V., Zakharov V.A.
Towards a unified toolset for embedded systems development.
Problems of Programming, N 1-2, 2000, p.316-322
- Бахмуров А.Г., Захаров В.А., Смелянский Р.Л., Чистолинов М.В.
О международном проекте в области проверки правильности
программного обеспечения встроенных систем.
Программные системы и инструменты, N 1, 2000, с.24-31.
- Захаров В.А., Кузюрин Н.Н., Холодов А.Н., Шабанов Л.В., Шокуров А.В.
Эффективные алгоритмы и их программные реализации.
Труды Ин-та системного программирования. N 1, 2000, с.115-124.
- Захаров В.А., Кончаков Р.В., Смелянский Р.Л., Царьков Д.В.
Верификация распределенных программ в системе имитационного моделирования DYANA.
Тезисы докладов Международной научной конференции "Интеллектуальные и многопроцессорные системы", с. 52-57.
- Захаров В.А., Коннов И.В. О верификации параметризованных симметричных систем распределенных программ.
Труды 1-ой Всероссийской научной конференции "Методы и средства обработки информации", Москва, 1-3 сентября 2003, 2003, с. 395-400.
- Захаров В.А., Корчевский А.А. Об одном символьном методе верификации криптографических протоколов.
Тезисы докладов XIV Международной конференции "Проблемы теоретической кибернетики", Пенза, 23-28 мая, 2005.
- Захаров В.А., Коннов И.В. Об одном подходе к верификации асинхронных параметризованных систем.
Труды 2-ой Всероссийской научной конференции "Методы и средства обработки информации", Москва, 2005, с. 367-373.
- Захаров В.А., Корчевский А.А. О формальной верификации криптографических протоколов с использованием spi-исчисления.
Труды 2-ой Всероссийской научной конференции "Методы и средства обработки информации", Москва, 2005, с. 373-379.
- Захаров В.А., Коннов И.В. Об одном подходе к верификации симметрических параметризованных распределенных систем.
Программирование, 2005, N 5.
- Булычев П.Е., Захаров В.А., Коннов И.В. Применение методов теории игр к поиску некоторых видов симуляции на размеченных системах переходов.
Труды VII международной конференции "Дискретные модели в теории управляющих систем", (Покровское, 4-6 марта, 2006 г.), 2006, с. 40-46.
- Bulychev P.E., Konnov I.V., Zakharov V.A. Computing (bi)simulation relations preserving CTL-X- logic for ordinary and fair Kripke structures.
Труды Института Системного программирования: Том 12. (под Ред. В.П Иванникова) - М.:ИСП РАН, 2007, с. 59-76.
- Konnov I.V., Zakharov V.A. On the verification of asynchronous parameterized networks of communicating processes by model checking.
Труды Института Системного программирования: Том 12. (под Ред. В.П Иванникова) - М.:ИСП РАН, 2007, с. 37-58.
- Konnov I.V., Zakharov V.A. An invariant-based approach to the verification of asynchronous parameterized networks.
Proceedings of the 1-st International Workshop on Invariant Generation, June 25-26, 2007, Hagenberg, Austria, 2007, p. 41-55.
- Булычев П.Е., Захаров В.А. Применение методов теории игр к поиску некоторых видов симуляции на размеченных системах
переходов с ограничениями справедливости.
Вестник МЭИ, т. 6, 2007. С. 5-9..
- Булычев П.Е., Захаров В.А. Об одной задаче верификации параметризованных конечных систем переходов.
Труды Третьей Всероссийской конференции "Методы и средства обработки информации", Москва, 2009, с. 98-104.
- Булычев П.Е., Захаров В.А. Универсальный подход к проверке отношений симуляции для моделей программ.
Труды Третьей Всероссийской конференции "Методы и средства обработки информации", Москва, 2009, с. 104-110.
- Булычев П.Е., Захаров В.А. О верификации конечных параметризованных моделей распределенных программ.
Научные ведомости Белгородского государственного университета, Серия История. Политология. Экономика. Информатика. 2009,
N 9, Вып. 11/1, с. 116-123.
-
Разрабатываются и исследуются методы анализа логических программ
публикации
- Захаров В.А., Маневич С.И. О преобразованиях операторных процедур в логические программы
Программирование, 1994, N 6, с.23-39.
- Zakharov V.A. On the refinement of logic programs by means of anti-unification
(ps)
Proceedings of the 2nd Panhellenic Logic Symposium, Delphi, Greece,
1999, p.219-224.
-
Статический анализ программ — это анализ программного обеспечения, производимый без
реального выполнения исследуемых программ. Цель анализа - обнаружить зависимости
по данным и по управлению между компонентами программы, которые можно использовать
впоследствии для компиляции, оптимизации, верификации программ.
публикации
- Захаров В.А. Вычисление инвариантов последовательных программ.
Тезисы докладов XIII Международной конференции «Проблемы теоретической кибернетики», Казань, Часть 1, 2002, с. 68.
- Захаров В.А., Костылев Е.В. Быстрые алгоритмы антиунификации и их применение при анализе программ
Материалы XIII Международной школы-семинара «Синтез и сложность управляющих систем», Пенза, Часть 1,
2002, с.76-81.
- Захаров В.А., Викторова М.С. Об одной системе вывода, связанной со статическим анализом программ.
Труды V Международной конференции "Дискретные модели в теории управляющих систем", (Ратмино, 26-29 мая 2003,
2003, с.19-21.
- Захаров В.А., Костылев Е.В. Об одном обобщении подстановок применительно к задаче синтеза инвариантов программ.
Материалы VIII Международного семинара "Дискретная математика и ее приложения",
Изд-во механико-математического ф-та МГУ, 2004, с. 134-137.
- Захаров В.А., Костылев Е.В. Об одном обобщении подстановки применительно к задаче статического анализа программ.
Вестник Московского университета, Серия Вычислительная математика и кибернетика, 2005, N 4, с.39-45.
- Захаров В.А., Костылев Е.В. О сложности задачи антиунификации.
Дискретная математика, Т. 20, вып. 1, 2008, с. 131-144.
- Khoroshilov A., Mutilin V., Shcherbina V., Strikov O., Vinogradov S., Zakharov V.A. How to cook an automated system for Linux driver verification.
Proceedings of the 1st Spring Young Researchers' Colloquium on Software Engineering SYRCoSE 2008 (St Petersburg, May 29-30, 2008),
2008, с. 15-19.
- Khoroshilov A., Mutilin V., Petrenko A.K., Zakharov V.A. Establishing Linux Driver Verification Processes .
Proceedings of the 7th International Conference "Perspectives of System Informatics", June 15-19, 2009, Novosibirsk,
Lecture Notes in Computer Science, v. 5947.
- Bulychev P.E., Kostylev E.V., Zakharov V.A. Anti-unification algorithms and their applications in program analysis.
Proceedings of the 7th International Conference "Perspectives of System Informatics", June 15-19, 2009, Novosibirsk,
Lecture Notes in Computer Science, v. 5947.
-
Конструируются и исследуются математические модели параллельных вычислений. Разрабатываются
математические методы анализа моделей параллельных вычислений.
публикации
- Захаров В.А., В.В.Спанопуло. О взаимосвязи двух семантик параллельных вычислений
(ps)
Программирование, 1997, N 6, с.36-48
- Zakharov V.A., Spanopulo V.V. To the Relationship between the Interleaving and Causal Models of
Parallel Computations
(ps)
Advances in Modal Logic'96, CSLI Publications,1997, p.221-232
- Захаров В.А., Незнанов И.К. О моделях систем взаимодействующих операторных программ
моделях
(ps)
Сборник трудов III Международной конференции "Дискретные модели в теории
управляющих систем", Красновидово-98, с.36-40
- Захаров В.А. О восстановлении процесса по последовательности срабатывания переходов
сети Петри
(ps)
Вестник Московского университета, сер. 15, Вычислительная математика и
кибернетика, 1998, N 4, с.31-34
- Захаров В.А., Кончаков Р.В. Формализация языка описания моделей распределенных систем программ
при помощи временных автоматов
Труды Всероссийской конференции"Высокопроизводительные вычисления и приложения",
Черноголовка, 30 Октября - 2 Ноября 2000 г, с. 151-157.
- Захаров В.А., Незнанов И.К. Операторные модели взаимодействующих процессов.
Математические вопросы кибернетики, Физматлит, вып.9, 2000.
- Захаров В.А., Кончаков Р.В. Теоретико-автоматный подход к определению формальных семантик языков программирования.
Труды Международной конференции "Параллельные вычисления и задачи управления" (РАСО'2001). Москва, 2-4 октября 2001 г.,
2001, с. 107-114.
- Chiobanu G., Zakharov V.A. Encoding mobile ambients into pi-calculus.
Proceedings of the Andrei Ershov 6th International Conference "Prespectives of System Informatics"
(27-30 June 2006, Novosibirsk), Lecture Notes in Computer Science, v. 4378, 2006, p. 148-161.
лекционные курсы
студенты и аспиранты
|
|