Pull to refresh

Comments 26

Да. Сверху так и написано — перевод.
Возможна ли эксплуатация этого бага in the wild для атаки отказа в обслуживании, как считаете?
Вряд ли, должно быть очень нетривиальное стечение обстоятельств. Во-первых, ошибка проявляется для довольно больших массивов из миллионов элементов, причём они должны быть специально сконструированы. Нечасто злоумышленник контролирует такой объём данных. Во-вторых, прямое последствие ошибки — это падение сортировки с исключением. При этом массив остаётся недосортированным, но данные все в нём лежат. Тут должна быть дополнительная проблема на атакуемой системе. К примеру, некорректная обработка исключения, в результате чего возникнет потеря данных. Или игнорирование исключения и выполнение на массиве дополнительного алгоритма, который предполагает, что массив отсортирован, и ведёт себя неадекватно, если это не так.
Это в Яве падение сортировки с исключением. А в Питоне?
А в питоне нужны слишком большие массивы ("Версия на CPython содержит ошибку,… алгоритм выделяет 85 элементов для runLen, и этого хватает (как показывает наш анализ в полной статье) для массивов, содержащих не более 2^49 элементов. Для сравнения, мощнейший на сегодняшний день суперкомпьютер Tianhe-2 обладает 2^50 байтами памяти.").
Для массива байтов 2^49 = 512 терабайт.
А разве нельзя делать функцию бинарного поиска на этапе сортировки массива?
Зачем массив нужно сначала отсортировать(упорядочить), а затем делать в нём поиск?
Часто бывает, что необходимо в одном и том же массиве искать много раз. Поэтому проще сперва один раз отсортировать, а затем быстро искать бинарным поиском. Если вам надо один раз поискать, проще вообще не сортировать, а перебрать все элементы линейно.
Давайте еще раз, я ошибся в package name java.util.Arrays.sort()

docs.oracle.com/javase/7/docs/api/java/util/Arrays.html
Кто-нибудь объясните человеку, далекому от Java, есть ли какой-то принцип, по которому выбирают, будет ли имя модуля в единственном числе или во множественном? Почему util в единственном, а Arrays во множественном?
Потому что util сокращение от utility, utils не имеет смысла.
А так обычно Lists заведует листами, List это как раз объект листа.
Аналогично есть Collections, Objects, Sets. Часть из них правда в Гуаве, но принцип понятен.
Аналогично Arrays заведует массивами, просто тут аналогичного объекта Array просто нет, но конвенция понятна.
Понятно, спасибо. Я больше по части C++ и для меня все наоборот: в util дофига утилит, поэтому его надо назвать utils, от utilities, что является довольно распространенным сокращением. Функции, заведующие списком я бы сделал статическими методами класса List, а для Array сделал бы класс только со статическими методами для единообразия.
java.util — это package
Collections, Objects и т.д. — это мода в Java по неимингу утильных классов(для Collection и Objects соответственно)

Почему это не сделали статическими методами? Скорее всего, потому что это не относится к сущностям, а именно утилиты. Ну и для разделения кода.
Оффтоп: В Java переносят хорошие практики из Guava — в Java 7 Objects появился, в Java 8, по моему, дополнили классы по работе с коллекциями. В общем, не может не радовать :)
Это не совсем так, то есть они действительно сделали Objects, но явно теоретики ибо допускают глупые косяки, что идею убивает. Например, как раз в тему, статический метод сравнения называется в Гуаве equal, а в Яве equals. И если гуавовскую версию можно сократить статик импортом и писать equal(a, b). То с явой не пройдет изза коллизии с обычным equals, не статическим. А полная форма слижком тяжеловесна. Правда, и в последней Гуаве почемуто этот метод переехал в MoreObjects. Но это так, к слову, ибо не мешает.
Много плюсов за статью, но ни одного комментария о самом инструменте формального анализа! Ведь это отличная вещь с великолепными потенциалом — один раз описываем контракт для метода и не беспокоимся о его содержимом — всё и так будет проверяться :)
А вообще кто-нибудь пользовался подобными вещами? Я так понял, это подобие контрактного программирования. Только более мощное. В IDEA есть аннотация Contract, которая позволяет выполнить простые проверки входных и выходных данных — описываем с помощью этой аннотации контракт для метода (что будет при подаче тех или иных значений), а дальше IDE сама проверят, что метод соответствует этому контракту.
Ну да, что-то похожее. В принципе объявление метода — уже мало-мальский контракт: вы говорите, какие аргументы каких типов метод принимает и какого типа результат вернёт, и сам компилятор следит за соблюдением контракта. Дальнейшее улучшение — аннотации типа jsr305 (Nonnull, Nonnegative), jcip (Immutable), контракты в IDEA и т. д. JML по сути существенное развитие этого подхода. Я сам не использовал, но могу предположить, что полная верификация в KeY может выполняться довольно долго и не всегда ответ будет типа «да/нет», чаще вы увидите набор дополнительных условий, которые KeY вывел, но сам доказать не смог. Кроме того, в описании контракта можно допустить ошибку так же, как в реализации. Поэтому в повседневной практике вряд ли разумно использовать такой инструмент. А вот для проверки алгоритмически сложного кода, который редко меняется — вполне сгодится.

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

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

Вообще формальные спецификации это очень мило и полезно, но в случае с PVS мозг мне изрядно взрывали, когда приходилось специфицировать операторы и функции, чтобы заработало всё остальное, бинарные операции например не были встроены, а когда доказываешь валидность shift-or… ахаха… хаха… ха…
Не понял героизма авторов (в оригинале куча заумных формул).
Чтобы написать правильный вариант, достаточно элементарной аккуратности.
Обозначим последовательность элементов в стеке цифрами 1,2,3,4.
Тройки 1,2,3 и 2,3,4 удовлетворяют некоторому соотношению — инварианту. (Двойки тоже, но их опускаем).
Добавляем к стеку элемент 5. Пусть тройка на конце (3,4,5) не удовлетворяет инварианту, выясняем, что сливать надо 3 и 4, обозначим результат как А. Теперь содержимое стека 1,2, А,5. Тройка на конце (2, А,5) удовлетворяет инварианту. Но какого хрена считать, что 1,2, А теперь тоже удовлетворяет инварианту?? Ясно, что нужно ее теперь проверять.

Во-первых, из ваших рассуждений лишь следует, что проверки трёх последних элементов недостаточно, но не следует, что проверки четырёх элементов достаточно (хотя это тоже можно доказать на пальцах). Во-вторых, тут получается вроде Колумбова яйца: когда решение известно, оно выглядит тривиальным. В классе TimSort почти 1000 строк и 15 методов. Найдёте ли вы с помощью элементарной аккуратности ошибку в таком объёме кода? А ведь авторы исследования даже не знали, есть ли ошибка.

Куча заумных формул — это да, математики же, они так разговаривают :-)
Ну да, я счел очевидным, что новое значение (А) не может испортить других инвариантов.

В целом я ориентировался на синтез правильного алгоритма, а не анализ готового чужого. Последнее, конечно, гораздо геморойнее.
А автоматически — так вообще супер.
Sign up to leave a comment.

Articles