Рассматривается становление информатики и аспектов компьютерной поддержки создания программного обеспечения, в том числе системных и прикладных программных систем, начиная от периода появления первых ЭВМ 1948-1990-х годов XX века. Рассмотрена программа информатизации России 1992 года и пути развития фундаментальных основ современных компьютерных наук или информатики и интеллектуализации разработки различных видов программных систем.

Обеспечение безопасности программного обеспечения является на сегодняшний день одной из первостепенных задач. Сбои в работе программного обеспечения могут привести к серьезным последствиям, а злонамеренная эксплуатация уязвимостей может причинить колоссальный ущерб. Крупные корпорации уделяют особое внимание анализу инцидентов информационной безопасности. Атаки повторного использования кода, основанные на возвратно-ориентированном программировании (ROP), приобретают всю большую популярность с каждым годом и могут быть применены даже в условиях работы защитных механизмов современных операционных систем. В отличие от обычного шелл-кода, где инструкции размещаются последовательно в памяти, ROP-цепочка состоит из множества маленьких блоков инструкций (гаджетов) и использует стек для связывания этих блоков, что затрудняет анализ ROP-эксплойтов. Целью данной работы является упрощение обратной инженерии ROP-эксплойтов. В этой статье предлагается метод анализа атак повторного использования кода, который позволяет восстановить семантику ROP-цепочки: разбить цепочку на гаджеты, определить семантику отдельных гаджетов и восстановить прототипы вызванных в ходе выполнения цепочки функций и системных вызовов и значения их аргументов. Семантика гаджета определяется его принадлежностью параметризованным типам. Каждый тип задается постусловием (булевым предикатом), которое должно быть всегда истинно после выполнения гаджета. Метод был реализован в виде программного инструмента и апробирован на реальных ROP-эксплойтах, найденных в интернете.

Ошибки при работе с библиотечными функциями обработки строк в языке Си являются частой причиной переполнения буфера, что в свою очередь нередко приводит к отказу в обслуживании, некорректной работе программы или появлению эксплуатируемой уязвимости. Одним из способов устранения различных ошибок на стадии разработки программы является статический анализ. Существующие методы статического анализа, ориентированные на работу со строками, либо не обеспечивают должный уровень истинных срабатываний, либо пропускают большое количество ошибок, либо неприменимы к промышленным программам большого размера, либо реализованы в рамках закрытых инструментов. Для наиболее полного покрытия дефектов в реальных программах необходимо обнаруживать ошибки, происходящие лишь на некоторых путях выполнения и не определяемые единственной точкой программы, и, кроме того, находить ошибки, связанные с некорректным использованием не только библиотечных, но и пользовательских функций. Целью данного исследования является построение алгоритма поиска ошибок при работе со строками, удовлетворяющего этим свойствам, ограничению на количество ложных срабатываний (не более 40%), применимого к любым программам на языке Си и масштабирующегося на проекты из нескольких миллионов строк. Для решения этой задачи был использован ранее разработанный подход символьного исполнения с объединением состояний, который был адаптирован для поддержки строковых операций. На основе алгоритма отслеживания операций с целыми числами был предложен алгоритм отслеживания длин строк. Разработанный алгоритм реализован в качестве одного из детекторов семейства детекторов переполнения буфера в рамках инструмента статического анализа Svace. В результате на тестовом наборе Juliet test suite на тестах, связанных с переполнением правой границы буфера, покрытие срабатываниями увеличилось с 15,4% до 41,5%, при этом не было выдано ни одного ложного предупреждения. По сравнению с известным анализатором Infer на наборе Juliet инструмент Svace без поддержки строк показывает приблизительно те же результаты, за исключением случая сложных циклов, а связанные со строками переполнения Infer, как правило, не находит.

В статье рассматриваются новый подход к получению дополнительной информации об исследуемом программном модуле на основе предварительного восстановления программной архитектуры в ходе анализа исполняемого кода. В результате появляется возможность сократить требования к затрачиваемым ресурсам за счёт ограничения области исследования, рационального выбора приоритетов, абстрагирования от второстепенных элементов. В работе демонстрируется осуществимость восстановления программной архитектуры в рамках двухэтапного процесса: вначале проводится выделение обособленных компонентов, а затем определяются их назначения и взаимоотношения. Предлагается автоматизированный метод декомпозиции программного модуля, позволяющий выделять компоненты, соответствующие статическим библиотекам, классам и их группам. Данный метод базируется на кластеризации функций по расстояниям между ними в адресном пространстве и на графе вызовов. Приведено описание реализации разработанного метода в виде плагина для дизассемблера IDA.

В рамках данной статьи описывается разработанная платформа для статического анализа бинарного кода. Платформа разработанa на основе межпроцедурного, потоко-чувствительного и контекстно-чувствительного анализа программы. В качестве промежуточного представления используется машинно-независимый язык REIL. На этом представлении разработаны и реализованы основные анализы потока данных - анализ достигающих определений, построение DEF-USE и USE-DEF цепочек, трансформация для удаления мертвого кода, анализ значений, анализ помеченных данных, анализа памяти и т.д. Реализованный подход аннотации функций позволяет распространять данные между вызовами функций, тем самым сделав анализ чувствительным к контексту. Платформа предоставляет программный интерфейс для работы со всеми реализованным анализами, что позволяет добавлять новые анализы в качестве плагинов.

В работе рассматривается подход к отслеживанию файловых операций с помощью перехвата запросов к виртуальному диску в эмуляторе. Такой способ позволяет получать информацию о файловых операциях независимо от гостевой ОС, однако требует отдельной реализации для каждой файловой системы. Важной проблемой для реализации данного подхода является корректная обработка изменений в файловой системе. С операционными системами, которые имеют свойство кешировать операции записи, возникают осложнения, так как операции записи могут выполняться в произвольном порядке. Для примера подхода был создан модуль эмулятора QEMU, отслеживающий операции с файловой системой ext3. Преимущество данного инструмента перед другими состоит в отсутствии вмешательства в работу ОС, а также отсутствии зависимости от ОС. Благодаря этому возможно использование на таких экзотических ОС, с которыми не работают другие инструменты мониторинга файловых операций. Предполагается, что модуль QEMU для файловых систем, отличных от ext2/3, может быть реализован с использованием методов, подобных описанным в статье.

В статье рассматриваются способы получения содержимого файлов, изменяемых в процессе работы известной среды динамического анализа с открытым исходным кодом Drakvuf. В Drakvuf изначально реализована функциональность сохранения файлов, основанная на использовании недокументированных механизмов работы с системным кэшем. Автором данной статьи предложен новый подход получения содержимого файлов в системах семейства Microsoft Windows с помощью Drakvuf. Предложенный подход основан исключительно на использовании публичного интерфейса ядра со стороны гипервизора и обеспечивает переносимость между различными версиями операционной системы. В завершение статьи приведены достоинства и недостатки обоих подходов, предложены направления дальнейших работ.

В статье представлены модели и алгоритмы обеспечения сквозного контроля качества сложных программно-технических систем (СПТС) посредством реализации программно-управляемого процесса разработки и верификации формальных моделей требований и архитектуры СПТС. Дан анализ научных публикаций и нормативно-методической базы в области разработки и применения на практике модельно-ориентированного подхода. Установлено, что наименее обеспеченными модельными, алгоритмическими и программными решениями являются вопросы, связанные с разработкой полного и корректного набора требований, а также с формализацией и верификацией технических проектов СПТС. Предложены способы решения существующих проблем посредством формирования единой модельно-языковой и информационно-программной среды разработки и верификации формальных моделей требований и архитектуры СПТС, построенных на основе оптимального набора взаимосвязанных fUML диаграмм, представленных в нотации языка ALF и верифицируемых в среде виртуальной машины fUML и с помощью SAT/SMT решателей.

В статье представлено описание модели управления доступом на языке темпоральной логики действий Лэмпорта, обеспечивающей выполнение требований мандатного контроля целостности и конфиденциальности с учетом информационных потоков по памяти. Отличительной особенностью модели является учет особенностей жизненного цикла электронных документов (задания прав к метаинформации и содержимому документа отдельно, ограничение числа копий документа). Для задания модели управления доступом был выбран язык темпоральной логики действий Лэмпорта, поскольку его нотация представляется наиболее близкой к общепринятой математической, выразительные возможности и инструментальные средства позволяют описывать и верифицировать системы, заданные в виде конечных автоматов. В модели определены следующие действия: создание/удаление субъекта, чтение, запись, дозапись ("слепая" запись), создание/удаление объекта, назначение/удаление прав доступа, вложение объекта в объект, исключение вложенного объекта, утверждение объекта (документа), отправка объекта (документа) в архив, отмена действия утвержденного объекта (документа), копирование объекта (документа). Также определены следующие инварианты: проверки типов (включает в себя проверку соответствия всех полей объектов, также проверку соответствия типу субъектов и проверку уникальности идентификаторов субъектов и объектов) и проверки безопасности (включает в себя проверку меток конфиденциальности и целостности взаимодействующих субъектов и объектов, а также корректность процедуры назначения прав доступа).

В рамках данной статьи рассматривается метамодель, лежащая в основе системы управления требованиями Requality. Базовая модель представляет собой дерево, каждой вершине которого сопоставлен набор именованных и типизированных свойств. Базовая модель проста и удобна для представления семантики набора требований, но оказывается не особо пригодной для формирования и сопровождения сколько-нибудь сложных каталогов требований. Поэтому авторами вводится набор декларативных моделей, позволяющих описывать каталог требований более компактным образом. При этом семантика декларативных моделей задаётся при помощи определения трансляции в базовую модель. Эти возможности обеспечивают гибкий инструментарий для компактного описания типовых наборов требований. Также в статье рассматриваются особенности реализации представленной метамодели в системе управления требованиями Requality. В заключении предлагается исследовать комбинацию представленной модели каталога требований с формальными моделями, позволяющими описывать семантику каждого требования в отдельности.

В данной работе представлено экспериментальное исследование эффективности ряда моделей нейронных сетей для задачи классификации побочных эффектов на уровне сущностей. Задача анализа тональности на уровне аспектных терминов, в которых необходимо определить мнение по отношению к конкретному аспекту, активно исследуется в течении последнего десятилетия. Для решения данной задачи в прошедшие годы было предложено несколько архитектур нейронных сетей. Несмотря на то, что модели, основанные на этих архитектурах, имеют много общего, есть некоторые компоненты, которые отличают их друг от друга. В данной статье была исследована применимость разработанных для аспектно ориентированного анализа тональности нейросетевых моделей для классификации побочных эффектов. Для оценки эффективности данных методов были проведены обширные эксперименты на различных англоязычных текстах биомедицинской тематики, включающих в себя записи клинических карточек, научную литературу и данные из социальных сетей. Также мы сравнили предлагаемую модель с одной из наилучших на данный момент моделей, основанной на методе опорных векторов и большом наборе признаков.

Рассматриваются вопросы численного моделирования нестационарных двухфазных потоков в пористых средах с существенно неоднородными свойствами с помощью численной схемы квазихарактеристик второго порядка аппроксимации. В отличие от известных схем высокого порядка, представленная схема имеет второй порядок аппроксимации в областях с большими градиентами решений, а также сохраняет монотонный характер решений. Это достигается за счет выбора итогового решения в каждой расчетной точке из нескольких допустимых решений с различными дисперсионными свойствами. Монотонный характер решения обеспечивается специальным критерием выбора решения, сформулированным в представленной работе. Этот критерий имеет локальный характер и удобен для параллельных вычислений. Эффективность подхода проиллюстрирована на решении задач вытеснения нефти водой в существенно неоднородных пористых пластах с коэффициентами абсолютной проницаемости, скачкообразно изменяющимися в десятки и сотни раз.

В последние годы в мировой практике существует тенденция к использованию специализированных CFD моделей в задачах вычислительной метеорологии. К таким задачам относится, в частности, задача обоснования безопасности промышленных объектов, в том числе радиационно-опасных. Эта тенденция обусловлена тем фактом, что применение универсальных инженерных кодов общего назначения требует изрядных вычислительных мощностей и связано это в первую очередь с необходимостью сгущения расчётной сетки к поверхностям земли и зданий для разрешения вязкого и промежуточного слоёв. С другой стороны, гауссовы модели не могут учесть сложные аэродинамические эффекты, возникающие при обтекании зданий сложной конфигурации, в том числе описать все тонкости обтекания сооружений примесью при атмосферных выбросах газо-аэрозольных веществ. Поэтому авторами была разработана робастная узкоспециализированная CFD-RANS модель и расчётный код для моделирования атмосферной дисперсии примеси в условиях сложной трёхмерной геометрии, не требующие сгущения сеток. Авторы работы провели верификацию этой модели на различных данных, полученных как в ходе натурных крупномасштабных, так и в ходе лабораторных туннельных экспериментов. Для этих целей была использована, в частности, рекомендованная международным экспертным сообществом база данных и соответствующие статистические характеристики соответствия рассчитанных и полученных в ходе экспериментов значения компонент скорости течения и концентрации примеси. Результаты верификации показали, что разработанная модель удовлетворяет приёмочным критериям качества моделирования наравне с зарубежными кодами общего назначения и узкоспециализированными кодами.

В работе приводятся результаты оценки возможности применения современных средств вычислительной гидромеханики для определения характеристик качки судна с шахтным устройством и колебаний жидкости в шахте на встречном волнении при отсутствии скорости хода. Шахтой называется «колодец», используемый на различных типах судов, таких как, кабелеукладочных, добычных и буровых, спасательных, исследовательских, снабжения и обеспечения. Эта шахта предназначена для спуска и подъема различного оборудования, водолазов или спасательных колоколов, кабелей или райзеров, защищенных от воздействия внешнего волнения. Результаты численного моделирования в программном комплексе OpenFOAM продольной качки модели DTMB 5415 на встречном регулярном волнении при наличии и отсутствия скорости хода показали, что численное моделирование позволяет с высокой эффективностью определять амплитудно-частотные и фазово-частотные характеристики вертикальной и килевой качки судна. Проведенное экспериментальное исследование модели серии 60 без шахты и с двумя шахтами круглого сечения различного диаметра на встречном волнении при отсутствии скорости хода позволило получить амплитудно-частотные характеристики вертикальной и килевой качки, а также вертикальных колебаний жидкости в шахте, которые показали, что влияние наличия шахты на динамику судна на встречном волнении пренебрежимо мало. Эти данные также необходимы для выполнения верификации численного моделирования колебаний судна с шахтой на встречном волнении. Численное моделирование экспериментального исследования показало, что современные средства вычислительной гидромеханики позволяют с хорошей эффективностью решать задачи по определению характеристик продольной качки судна, снабженного шахтным устройством, и вертикальных колебаний жидкости в шахте на встречном волнении при отсутствии скорости хода. Численное моделирование качки судна с шахтным устройством может быть рекомендовано на начальных стадиях проектирования для определения параметров качки и вертикальных колебаний жидкости в шахте.

На основе RDF-хранилища создан программный комплекс для формирования базы знаний, содержащей информацию о проведенных гидрогазодинамических расчетах. Комплекс представляет собой набор скриптов, написанных на языке bash и python, которые опубликованы под открытой лицензией GNU GPL 3. Инструмент предназначен для поддержки расчетчика при проведении поисковых исследований, не имеющих строгого, наперед заданного плана эксперимента или алгоритма решения задачи. Для формализации описания расчета, хранящегося в базе знаний, создана онтология, служащая его информационной моделью. В качестве вспомогательного средства для проведения автоматизированного сравнения расчетов друг с другом разработан механизм «компараторов» и «особенностей», также описанный в статье. Помимо систематизированного хранения данных комплекс обеспечивает возможность их автоматического и полуавтоматического анализа, в том числе представление банка расчетов в форме неориентированного графа, построение плоских и пространственных зависимостей, поиск сходных расчетов и т.п. В статье приводятся примеры обработки данных проекта по профилированию каналов в головке цилиндров поршневого двигателя.

В статье рассматривается подход к проверке функциональных свойств смарт-контрактов платформы Ethereum методом символьной верификации модели. Описанный подход позволяет верифицировать выполнение 3х видов свойств на трассах ограниченной длины, а также осуществлять проверку выполнимости инварианта. Описана математическая модель среды исполнения смарт-контрактов, проведена формализация выделенных видов свойств в рамках этой модели, описана процедура трансляции всего перечисленного в язык ограничений SMT-решателя. Жизнеспособность предлагаемого подхода иллюстрируется на примере верификации макетного смарт-контракта MiniDAO, упрощённой версии известного TheDAO. За несколько секунд макет находит контр пример одному нетривиальному функциональному требованию, указывая на ошибку в бизнес-логике смарт-контракта. Насколько нам известно, эта работа - одна из первых попыток описать инструмент, помогающий осуществлять формальную проверку функциональных свойств смарт-контрактов в автоматическом режиме.