Рубрика «поиск уязвимостей»

На мой взгляд, в русскоязычном секторе интернета тематика формальной верификации освещена недостаточно, и особенно не хватает простых и наглядных примеров.

Я приведу такой пример из зарубежного источника, и дополню собственным решением известной задачи о переправе волка, козы и капусты на другую сторону реки.

Но вначале вкратце опишу, что из себя представляет формальная верификация и зачем она нужна.

Под формальной верификацией обычно понимают проверку одной программы либо алгоритма с помощью другой.

Это нужно для того, чтобы удостовериться, что поведение программы соответствует ожидаемому, а также обеспечить её безопасность.

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

Однако в любом случае будет получен один из трёх ответов: программа корректна, некорректна, или же — вычислить ответ не удалось.

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

А применяется формальная верификация, например, в ядре Windows и операционных системах беспилотников Darpa, для обеспечения максимального уровня защиты.

Мы будем использовать Z3Prover, очень мощный инструмент для автоматизированного доказательства теорем и решения уравнения.

Причём Z3 именно решает уравнения, а не подбирает их значения грубым брутфорсом.
Это означает, что он способен находить ответ, даже в случаях когда комбинаций входных вариантов и 10^100.

А ведь это всего лишь около дюжины входных аргументов типа Integer, и подобное зачастую встречается на практике.

Задача о 8 ферзях (Взята из англоязычного мануала).

Формальная верификация на примере задачи о волке, козе и капусте - 1
Читать полностью »

Последнее время все чаще говорят о статическом анализе как одном из важных средств обеспечения качества разрабатываемых программных продуктов, особенно с точки зрения безопасности. Статический анализ позволяет находить уязвимости и другие ошибки, его можно использовать в процессе разработки, интегрируя в настроенные процессы. Однако в связи с его применением возникает много вопросов. Чем отличаются платные и бесплатные инструменты? Почему недостаточно использовать линтер? В конце концов, при чем тут статистика? Попробуем разобраться.

О статическом анализе начистоту - 1
Читать полностью »

image


Мировой лидер производства дронов DJI объявил о том, что готов заплатить от 100 долларов до 30000 долларов за найденные «уязвимости». Пока сайт с подробным описанием «охоты за багами» в разработке, писать о найденных дырах надо писать на почту — bugbounty@dji.com

Директор по техническим стандартам DJI Уолтер Стоквел сказал, что вместо того, чтобы бороться с хакерами, нужно использовать их наработки и достижения, чтобы совместно двигаться к общей цели в рамках миссии компании.

«Я уверен, монсеньор, наконец-то, понял.»
— «Святые из трущоб»

На самом деле руководство DJI зашевелилось после нескольких громких косяков с киберуязвимостями и «баном» со стороны американских военных.
Читать полностью »

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

Некорректное завершение работы программы в ходе фаззинга позволяет сделать предположение о наличии уязвимости.

В этой статье мы:

  • продемонстрируем, как фаззить обработчик JSON-запросов;
  • используя фаззинг, найдём уязвимость переполнения буфера;
  • напишем шеллкод на Ассемблере для эксплуатации найденной уязвимости.

Разбирать будем на примере исходных данных задания прошлого NeoQUEST. Известно, что 64-хбитный Linux-сервер обрабатывает запросы в формате JSON, которые заканчиваются нуль-терминатором (символом с кодом 0). Для получения ключа требуется отправить запрос с верным паролем, при этом доступа к исходным кодам и к бинарнику серверного процесса нет, даны только IP-адрес и порт. В легенде к заданию также было указано, что MD5-хеш правильного пароля содержится где-то в памяти процесса после следующих 5 символов: «hash:». А для того, чтобы вытащить пароль из памяти процесса, необходима возможность удалённого исполнения кода.
Читать полностью »

Эта статья будет ответом на недавнюю публикацию Владимира Таратушка.
Причин написания статьи у меня было несколько.
Первая — это показать, что белые хакеры в Украине есть. Существуют они благодаря одной из программ поощрения поиска уязвимостей, которую проводит Приватбанк.
Следующая причина — это рассказать свою success story работы с одним из крупнейшим банком Украины в рамках данной программы.
Так же я хочу показать эффективность работы такой программы на реальном примере и сподвигнуть к организации таких программ те компании, которые по каким то причинам сомневаются или не видят в них реальных плюсов.
Ну и последняя причина — показать будущим и настоящим ресёчерам, что участие в баг-баунти программах интересно, этично и материально выгодно.
Читать полностью »

Vulners — Гугл для хакера. Как устроен лучший поисковик по уязвимостям и как им пользоваться - 1

Часто нужно узнать всю информацию о какой-нибудь уязвимости: насколько найденная бага критична, есть ли готовые сплоиты, какие вендоры уже выпустили патчи, каким сканером проверить ее наличие в системе. Раньше приходилось искать вручную по десятку источников (CVEDetails, SecurityFocus, Rapid7 DB, Exploit-DB, базы уязвимостей CVE от MITRE/NIST, вендорские бюллетени) и анализировать собранные данные. Сегодня эту рутину можно (и нужно!) автоматизировать с помощью специализированных сервисов. Один из таких — Vulners, крутейший поисковик по багам. А главное — бесплатный и с открытым API. Посмотрим, чем он может быть нам полезен.
Читать полностью »

Решето под названием Adobe Flash - 1 Пока еще широко распространенный продукт Flash Player компании Adobe печально известен своей безопасностью. Регулярно становится известно об очередной zero-day уязвимости во Flash, используемой хакерами в APT-кампаниях. 2015 год выдался особенно урожайным на такие уязвимости. Большая доля критических RCE-уязвимостей были вызваны некорректной работой с памятью: была возможна запись в освобожденную память в куче процесса Flash.

В этой статье мы поисследовали безопасность Adobe Flash и выяснили, что многие его «дыры в безопасности» — хронические, и решить их можно разве что переписыванием кода с нуля, в то время как разработчики ставят заплатку на заплатку, что, конечно, не повышает уровень безопасности. А еще мы продемонстрируем некоторые найденные нами и незакрытые на данный момент уязвимости!
Читать полностью »

С сегодняшнего дня у нас появились реальные рычаги, которые позволят заставить банки «залатать дыры» в своем ПО, а также сменить устаревшее железо.
Читать полностью »

Одним из методов поиска уязвимостей в программном обеспечении является использование анализаторов исходных текстов. В данной посте хочу рассказать об одном из них, а именно о RATS (Rough Auditing Tool for Security). Начать именно с этой утилиты, решил потому что упоминания о ней встречались не раз в уважаемых мной источниках, а именно тут, тут и еще здесь. Однако реального примера использования нигде не было, поэтому я решил рассказать о RATS подробнее.
Читать полностью »

Безопасность продуктов — один из главных приоритетов Google. Мы по умолчанию используем надежное шифрование на базе SSL для таких сервисов, как Поиск, Gmail и Google Диск. Все данные, которыми обмениваются наши дата-центры, также зашифрованы. Но кроме безопасности наших собственных продуктов нас волнует безопасность Интернета в целом. Именно поэтому сотрудники компании уделяют большое внимание поиску уязвимостей в Сети и даже объединяют информацию о них в отчеты. В первую очередь это касается поиска ошибок типа Heartbleed.

Результаты этого небольшого и, в общем-то, стороннего проекта показались нам настолько интересными, что мы решили собрать новую команду специалистов под общим названием «Проект Ноль».

Пользуясь Интернетом, вы должны быть уверены, что никто не смог воспользоваться ошибками в коде, чтобы запустить вирус в ваш компьютер, получить доступ к закрытой информации или отследить ваши контакты. К сожалению, в мире существует немало сложных вредоносных программ, например программы под общим названием «Уязвимость нулевого дня», которые уже были использованы против борцов за права человека или в целях промышленного шпионажа. Мы считаем, что такой практике нужно положить конец, и готовы работать над решением этой проблемы.

«Проект Ноль» – это первый шаг, который станет нашим вкладом в общее дело. Наша цель – значительно сократить количество людей, пострадавших от целевых атак. Мы приглашаем на работу лучших специалистов-практиков в области исследований проблем сетевой безопасности, а они, в свою очередь, посвящают 100% своего рабочего времени повышению уровня безопасности в Интернете.
Читать полностью »


https://ajax.googleapis.com/ajax/libs/jquery/3.4.1/jquery.min.js