Сообщение Re: Проблема остановки и память от 18.09.2015 8:04
Изменено 18.09.2015 8:07 kochetkov.vladimir
Здравствуйте, Куть, Вы писали:
К>У меня 3 вопроса:
К>1. Есть ли ошибки в моём доказательстве?
С теоретической точки зрения — нет, все верно. Более того, схожие рассуждения имеют место во многих работах, например у Бишопа и сотоваришей: http://nob.cs.ucdavis.edu/bishop/notes/2008-cse-14/2008-cse-14.pdf По сути, они там приходят к тому, что доказать незащищенность программы (задача, сводимая к проблеме останова) возможно только прогнав ее через все возможные наборы входных данных и контролируя множество конфигураций, в которые при этом входит машина. С инженерной же точки зрения, в подобных рассуждениях мало пользы, поскольку, как уже упомянул Cyberax, в этом случае задача сводится к поиску циклов в графе состояний конечного автомата, количество вершин в котором растет по формуле S^N*X, где S — размер входного алфавита, N — количество доступной памями и X — количество состояний в программе МТ. Поэтому при решении реальных задач анализа кода стремятся максимально огрубить понятие "состояние" с тем, чтобы сократить их возможное количество, не теряя при этом в точности результатов. Как правило, для этого прибегают к группировке схожих состояний по каким-либо признакам и далее рассматривают каждую группу, как если бы это было одно состояние.
К>2. Может ли иметь теоретическое или практическое применение Анализатор для программ с конечной памятью?
Конечно. Например в анализаторе, разрабатываемом нами, используется символическая интерпретация и частично-конкретное выполнение анализируемого кода, в результате чего мы получаем граф потока управления, в вершинах которого описываются множества значений всех потоков данных, доступных в данной точке выполнения. По сути — это и есть верхнеуровневый аналог состояния программы. Далее мы строим по этим состояниям формулу достижимости того или иного пути в графе, приводящего к потенциальной уязвимости и решаем их на SMT-солвере. Из решения такой формулы тривиально генерируется как эксплоит для существующей уязвимости, так и патч, закрывающий ее. Подробнее рассказывал об этом здесь и здесь (запись также есть тут).
К>3. Что ломается в доказательствах неразрешимости при ограничении памяти?
Как уже сказали выше, все
К>У меня 3 вопроса:
К>1. Есть ли ошибки в моём доказательстве?
С теоретической точки зрения — нет, все верно. Более того, схожие рассуждения имеют место во многих работах, например у Бишопа и сотоваришей: http://nob.cs.ucdavis.edu/bishop/notes/2008-cse-14/2008-cse-14.pdf По сути, они там приходят к тому, что доказать незащищенность программы (задача, сводимая к проблеме останова) возможно только прогнав ее через все возможные наборы входных данных и контролируя множество конфигураций, в которые при этом входит машина. С инженерной же точки зрения, в подобных рассуждениях мало пользы, поскольку, как уже упомянул Cyberax, в этом случае задача сводится к поиску циклов в графе состояний конечного автомата, количество вершин в котором растет по формуле S^N*X, где S — размер входного алфавита, N — количество доступной памями и X — количество состояний в программе МТ. Поэтому при решении реальных задач анализа кода стремятся максимально огрубить понятие "состояние" с тем, чтобы сократить их возможное количество, не теряя при этом в точности результатов. Как правило, для этого прибегают к группировке схожих состояний по каким-либо признакам и далее рассматривают каждую группу, как если бы это было одно состояние.
К>2. Может ли иметь теоретическое или практическое применение Анализатор для программ с конечной памятью?
Конечно. Например в анализаторе, разрабатываемом нами, используется символическая интерпретация и частично-конкретное выполнение анализируемого кода, в результате чего мы получаем граф потока управления, в вершинах которого описываются множества значений всех потоков данных, доступных в данной точке выполнения. По сути — это и есть верхнеуровневый аналог состояния программы. Далее мы строим по этим состояниям формулу достижимости того или иного пути в графе, приводящего к потенциальной уязвимости и решаем их на SMT-солвере. Из решения такой формулы тривиально генерируется как эксплоит для существующей уязвимости, так и патч, закрывающий ее. Подробнее рассказывал об этом здесь и здесь (запись также есть тут).
К>3. Что ломается в доказательствах неразрешимости при ограничении памяти?
Как уже сказали выше, все
... << RSDN@Home 1.2.0 alpha 5 rev. 76>>
Re: Проблема остановки и память
Здравствуйте, Куть, Вы писали:
К>У меня 3 вопроса:
К>1. Есть ли ошибки в моём доказательстве?
С теоретической точки зрения — нет, все верно. Более того, схожие рассуждения имеют место во многих работах, например у Бишопа и сотоваришей: http://nob.cs.ucdavis.edu/bishop/notes/2008-cse-14/2008-cse-14.pdf По сути, они там приходят к тому, что доказать незащищенность программы (задача, сводимая к проблеме останова) возможно только прогнав ее через все возможные наборы входных данных и контролируя множество конфигураций, в которые при этом входит машина. С инженерной же точки зрения, в подобных рассуждениях мало пользы, поскольку, как уже упомянул Cyberax, в этом случае задача сводится к поиску циклов в графе состояний конечного автомата, количество вершин в котором растет по формуле S^N*X, где S — размер входного алфавита, N — количество доступной памями и X — количество состояний в программе МТ. Поэтому при решении реальных задач анализа кода стремятся максимально огрубить понятие "состояние" с тем, чтобы сократить их возможное количество, не теряя при этом в точности результатов. Как правило, для этого прибегают к группировке схожих состояний по каким-либо признакам и далее рассматривают каждую группу, как если бы это было одно состояние.
К>2. Может ли иметь теоретическое или практическое применение Анализатор для программ с конечной памятью?
Конечно. Например в анализаторе, разрабатываемом нами, используется символическая интерпретация и частично-конкретное выполнение анализируемого кода для построения графа потока управления, в вершинах которого описываются множества значений всех потоков данных, доступных в данной точке выполнения. По сути, это и есть верхнеуровневый аналог состояния программы. Далее мы строим по этим состояниям формулу достижимости того или иного пути в графе, приводящего к потенциальной уязвимости и решаем ее на SMT-солвере. Из решения такой формулы тривиально генерируется как эксплоит для существующей уязвимости, так и патч, закрывающий ее. Подробнее рассказывал об этом здесь и здесь (запись также есть тут).
К>3. Что ломается в доказательствах неразрешимости при ограничении памяти?
Как уже сказали выше, все
К>У меня 3 вопроса:
К>1. Есть ли ошибки в моём доказательстве?
С теоретической точки зрения — нет, все верно. Более того, схожие рассуждения имеют место во многих работах, например у Бишопа и сотоваришей: http://nob.cs.ucdavis.edu/bishop/notes/2008-cse-14/2008-cse-14.pdf По сути, они там приходят к тому, что доказать незащищенность программы (задача, сводимая к проблеме останова) возможно только прогнав ее через все возможные наборы входных данных и контролируя множество конфигураций, в которые при этом входит машина. С инженерной же точки зрения, в подобных рассуждениях мало пользы, поскольку, как уже упомянул Cyberax, в этом случае задача сводится к поиску циклов в графе состояний конечного автомата, количество вершин в котором растет по формуле S^N*X, где S — размер входного алфавита, N — количество доступной памями и X — количество состояний в программе МТ. Поэтому при решении реальных задач анализа кода стремятся максимально огрубить понятие "состояние" с тем, чтобы сократить их возможное количество, не теряя при этом в точности результатов. Как правило, для этого прибегают к группировке схожих состояний по каким-либо признакам и далее рассматривают каждую группу, как если бы это было одно состояние.
К>2. Может ли иметь теоретическое или практическое применение Анализатор для программ с конечной памятью?
Конечно. Например в анализаторе, разрабатываемом нами, используется символическая интерпретация и частично-конкретное выполнение анализируемого кода для построения графа потока управления, в вершинах которого описываются множества значений всех потоков данных, доступных в данной точке выполнения. По сути, это и есть верхнеуровневый аналог состояния программы. Далее мы строим по этим состояниям формулу достижимости того или иного пути в графе, приводящего к потенциальной уязвимости и решаем ее на SMT-солвере. Из решения такой формулы тривиально генерируется как эксплоит для существующей уязвимости, так и патч, закрывающий ее. Подробнее рассказывал об этом здесь и здесь (запись также есть тут).
К>3. Что ломается в доказательствах неразрешимости при ограничении памяти?
Как уже сказали выше, все
... << RSDN@Home 1.2.0 alpha 5 rev. 76>>