Сообщение Re[18]: А если бы все с начала ? от 29.01.2018 23:09
Изменено 29.01.2018 23:12 kochetkov.vladimir
Re[18]: А если бы все с начала ?
Здравствуйте, WolfHound, Вы писали:
WH>Покажи в каком месте моего кода находится эта модель?
Её и не должно быть в коде. Инварианты и пред-/пост-условия, используемые в рамках формальной верификации, всегда описывают свойства некоторой подразумеваемой эталонной модели предметной области, относительно которой осуществляется верификация. В простейших случаях, типа сортировки, в явном построении этой модели нет необходимости, т.к. её свойства формулируются интуитивно. Если же говорить о верификации реальных систем, то там без построения такой модели обойтись не получится. Например, для верификации компилятора какого-либо языка, необходимо формальное описание, как грамматики языка, так и его семантики: денотационной -- для верификации компилятора относительно матмодели языка, интерпретационной -- для верификации кодогенератора, трансформационной -- для верификации средств метапрограммирования или транскомпиляции и т.п. Всё это вместе и составляет первую часть той модели, о которой я говорил.
WH>Я не знаю ничего про TLS, но HTTP это же почти регулярный язык.
WH>Из того что там не регулярное:
WH>1)Прочитать число и считать количество байт равное этому числу.
И это уже делает HTTP контекстно-зависимым языком (см. https://pdfs.semanticscholar.org/7d95/6ddef192f3a10b22bc41044566be396c751f.pdf, п3.3), для разбора которого требуется LBA, суть -- машина Тьюринга с ограниченной памятью.
WH>Вот предикаты, которым должны соответствовать все сортировки. Верифицировать их нужно глазами. Благо они очень простые.
Они действительно простые, но только потому, что простыми в данном примере являются формулы определения отношения частичного порядка на множестве элементов, выступающие здесь в роли первой части упомянутой модели.
WH>//Предикат который утверждает что функция переставляет местами элементы массива [begin..end)
WH>//и не меняет остальной массив
И вот тут мы приходим ко второй части модели. Если опираться на определение понятия алгоритма из теории формальных языков (т.е. что всякий алгоритм является распознавателем какого-либо формального языка), то первая часть лишь доказывает, что верифицируемый алгоритм распознаёт полное множество слов, принадлежащих некоторому языку. Но нам также надо ещё и доказать, что этот же алгоритм не распознаёт слова, принадлежащие дополнению данного языка. Дополнение КЗ-языка является КЗ-языком -> ещё одна МТ с ограниченной памятью, отсутствие которой нужно доказать. А доказать отсутствие чего-либо в общем случае "гораздо труднее", чем наличие
Опять-таки, в случае сортировки вполне достаточно сказать "алгоритм может переставлять элементы входного массива, как ему вздумается, лишь бы на выходе всегда был упорядоченный массив", опираясь на допущение, что сортировка -- не более чем цепочка последовательных перестановок элементов некоторого множества. А как быть, даже в таком случае, как, к примеру, режимы блочного шифрования с обратной связью, где каждый последующий блок шифротекста является результатом нетривиальных операций между промежуточным блоком и всеми или некоторыми предыдущими?
Для верификации криптографии, кстати, на практике используются специально заточенные под эту задачу DSL'и. Такие, как https://github.com/GaloisInc/cryptol, например. Просто потому, что описать даже примитивные криптоалгоритмы традиционными средствами верификации невероятно тяжело. И это при том, что за любым таким алгоритмом стоит совершенно строгая формальная модель. Что касается прочих классов уязвимостей, то частичные модели на данный момент, построены только для инъекций, некоторых подклассов атак повреждения памяти и гонок за ресурсами. Для всех остальных классов моделей нет, а значит и нет возможности верифицировать код на предмет их отсутствия.
WH>Ну и на практике нам нужно верифицировать не всё, а только некоторые свойства программы. Такие как не выход за приделы массива.
Уязвимость -- есть множество достижимых состояний приложения (конфигураций в терминологии Тьюринга), в которых для любого информационного потока нарушается любое из свойств защищённости (в общепринятой модели угроз это -- конфиденциальность, доступность, целостность, авторизованность и аутентичность). Для того, чтобы доказать безопасность приложения средствами частичной формальной верификации (т.е. когда верифицируется не всё), мы должны помимо всего прочего ещё и доказать, что верификация покрывает всё множество таких состояний. Не буду утверждать, что это неразрешимая проблема (хотя, IMO, так оно и есть), но вот то, что известных способов её решения на данный момент не существует -- совершенно точно.
WH>Покажи в каком месте моего кода находится эта модель?
Её и не должно быть в коде. Инварианты и пред-/пост-условия, используемые в рамках формальной верификации, всегда описывают свойства некоторой подразумеваемой эталонной модели предметной области, относительно которой осуществляется верификация. В простейших случаях, типа сортировки, в явном построении этой модели нет необходимости, т.к. её свойства формулируются интуитивно. Если же говорить о верификации реальных систем, то там без построения такой модели обойтись не получится. Например, для верификации компилятора какого-либо языка, необходимо формальное описание, как грамматики языка, так и его семантики: денотационной -- для верификации компилятора относительно матмодели языка, интерпретационной -- для верификации кодогенератора, трансформационной -- для верификации средств метапрограммирования или транскомпиляции и т.п. Всё это вместе и составляет первую часть той модели, о которой я говорил.
WH>Я не знаю ничего про TLS, но HTTP это же почти регулярный язык.
WH>Из того что там не регулярное:
WH>1)Прочитать число и считать количество байт равное этому числу.
И это уже делает HTTP контекстно-зависимым языком (см. https://pdfs.semanticscholar.org/7d95/6ddef192f3a10b22bc41044566be396c751f.pdf, п3.3), для разбора которого требуется LBA, суть -- машина Тьюринга с ограниченной памятью.
WH>Вот предикаты, которым должны соответствовать все сортировки. Верифицировать их нужно глазами. Благо они очень простые.
Они действительно простые, но только потому, что простыми в данном примере являются формулы определения отношения частичного порядка на множестве элементов, выступающие здесь в роли первой части упомянутой модели.
WH>//Предикат который утверждает что функция переставляет местами элементы массива [begin..end)
WH>//и не меняет остальной массив
И вот тут мы приходим ко второй части модели. Если опираться на определение понятия алгоритма из теории формальных языков (т.е. что всякий алгоритм является распознавателем какого-либо формального языка), то первая часть лишь доказывает, что верифицируемый алгоритм распознаёт полное множество слов, принадлежащих некоторому языку. Но нам также надо ещё и доказать, что этот же алгоритм не распознаёт слова, принадлежащие дополнению данного языка. Дополнение КЗ-языка является КЗ-языком -> ещё одна МТ с ограниченной памятью, отсутствие которой нужно доказать. А доказать отсутствие чего-либо в общем случае "гораздо труднее", чем наличие
Опять-таки, в случае сортировки вполне достаточно сказать "алгоритм может переставлять элементы входного массива, как ему вздумается, лишь бы на выходе всегда был упорядоченный массив", опираясь на допущение, что сортировка -- не более чем цепочка последовательных перестановок элементов некоторого множества. А как быть, даже в таком случае, как, к примеру, режимы блочного шифрования с обратной связью, где каждый последующий блок шифротекста является результатом нетривиальных операций между промежуточным блоком и всеми или некоторыми предыдущими?
Для верификации криптографии, кстати, на практике используются специально заточенные под эту задачу DSL'и. Такие, как https://github.com/GaloisInc/cryptol, например. Просто потому, что описать даже примитивные криптоалгоритмы традиционными средствами верификации невероятно тяжело. И это при том, что за любым таким алгоритмом стоит совершенно строгая формальная модель. Что касается прочих классов уязвимостей, то частичные модели на данный момент, построены только для инъекций, некоторых подклассов атак повреждения памяти и гонок за ресурсами. Для всех остальных классов моделей нет, а значит и нет возможности верифицировать код на предмет их отсутствия.
WH>Ну и на практике нам нужно верифицировать не всё, а только некоторые свойства программы. Такие как не выход за приделы массива.
Уязвимость -- есть множество достижимых состояний приложения (конфигураций в терминологии Тьюринга), в которых для любого информационного потока нарушается любое из свойств защищённости (в общепринятой модели угроз это -- конфиденциальность, доступность, целостность, авторизованность и аутентичность). Для того, чтобы доказать безопасность приложения средствами частичной формальной верификации (т.е. когда верифицируется не всё), мы должны помимо всего прочего ещё и доказать, что верификация покрывает всё множество таких состояний. Не буду утверждать, что это неразрешимая проблема (хотя, IMO, так оно и есть), но вот то, что известных способов её решения на данный момент не существует -- совершенно точно.
Re[18]: А если бы все с начала ?
Здравствуйте, WolfHound, Вы писали:
WH>Покажи в каком месте моего кода находится эта модель?
Её и не должно быть в коде. Инварианты и пред-/пост-условия, используемые в рамках формальной верификации, всегда описывают свойства некоторой подразумеваемой эталонной модели предметной области, относительно которой осуществляется верификация. В простейших случаях, типа сортировки, в явном построении этой модели нет необходимости, т.к. её свойства формулируются интуитивно. Если же говорить о верификации реальных систем, то там без построения такой модели обойтись не получится. Например, для верификации компилятора какого-либо языка, необходимо формальное описание, как грамматики языка, так и его семантики: денотационной -- для верификации компилятора относительно матмодели языка, интерпретационной -- для верификации кодогенератора, трансформационной -- для верификации средств метапрограммирования или транскомпиляции и т.п. Всё это вместе и составляет первую часть той модели, о которой я говорил.
WH>Я не знаю ничего про TLS, но HTTP это же почти регулярный язык.
WH>Из того что там не регулярное:
WH>1)Прочитать число и считать количество байт равное этому числу.
И это уже делает HTTP контекстно-зависимым языком (см. https://pdfs.semanticscholar.org/7d95/6ddef192f3a10b22bc41044566be396c751f.pdf, п3.3), для разбора которого требуется LBA, суть -- машина Тьюринга с ограниченной памятью.
WH>Вот предикаты, которым должны соответствовать все сортировки. Верифицировать их нужно глазами. Благо они очень простые.
Они действительно простые, но только потому, что простыми в данном примере являются формулы определения отношения частичного порядка на множестве элементов, выступающие здесь в роли первой части упомянутой модели.
WH>//Предикат который утверждает что функция переставляет местами элементы массива [begin..end)
WH>//и не меняет остальной массив
И вот тут мы приходим ко второй части модели. Если опираться на определение понятия алгоритма из теории формальных языков (т.е. что всякий алгоритм является распознавателем какого-либо формального языка), то первая часть лишь доказывает, что верифицируемый алгоритм распознаёт полное множество слов, принадлежащих некоторому языку. Но нам также надо ещё и доказать, что этот же алгоритм не распознаёт слова, принадлежащие дополнению данного языка. Дополнение КЗ-языка является КЗ-языком -> ещё одна МТ с ограниченной памятью, отсутствие которой нужно доказать. А доказать отсутствие чего-либо в общем случае "гораздо труднее", чем наличие
Опять-таки, в случае сортировки вполне достаточно сказать "алгоритм может переставлять элементы входного массива, как ему вздумается, лишь бы на выходе всегда был упорядоченный массив", опираясь на допущение, что сортировка -- не более чем цепочка последовательных перестановок элементов некоторого множества. А как быть, даже в таком относительно простом случае, как, к примеру, режимы блочного шифрования с обратной связью, где каждый последующий блок шифротекста является результатом нетривиальных операций между промежуточным блоком и всеми или некоторыми предыдущими?
Для верификации криптографии, кстати, на практике используются специально заточенные под эту задачу DSL'и. Такие, как https://github.com/GaloisInc/cryptol, например. Просто потому, что описать даже примитивные криптоалгоритмы традиционными средствами верификации невероятно тяжело. И это при том, что за любым таким алгоритмом стоит совершенно строгая формальная модель. Что касается прочих классов уязвимостей, то частичные модели на данный момент, построены только для инъекций, некоторых подклассов атак повреждения памяти и гонок за ресурсами. Для всех остальных классов моделей нет, а значит и нет возможности верифицировать код на предмет их отсутствия.
WH>Ну и на практике нам нужно верифицировать не всё, а только некоторые свойства программы. Такие как не выход за приделы массива.
Уязвимость -- есть множество достижимых состояний приложения (конфигураций в терминологии Тьюринга), в которых для любого информационного потока нарушается любое из свойств защищённости (в общепринятой модели угроз это -- конфиденциальность, доступность, целостность, авторизованность и аутентичность). Для того, чтобы доказать безопасность приложения средствами частичной формальной верификации (т.е. когда верифицируется не всё), мы должны помимо всего прочего ещё и доказать, что верификация покрывает всё множество таких состояний. Не буду утверждать, что это неразрешимая проблема (хотя, IMO, так оно и есть), но вот то, что известных способов её решения на данный момент не существует -- совершенно точно.
WH>Покажи в каком месте моего кода находится эта модель?
Её и не должно быть в коде. Инварианты и пред-/пост-условия, используемые в рамках формальной верификации, всегда описывают свойства некоторой подразумеваемой эталонной модели предметной области, относительно которой осуществляется верификация. В простейших случаях, типа сортировки, в явном построении этой модели нет необходимости, т.к. её свойства формулируются интуитивно. Если же говорить о верификации реальных систем, то там без построения такой модели обойтись не получится. Например, для верификации компилятора какого-либо языка, необходимо формальное описание, как грамматики языка, так и его семантики: денотационной -- для верификации компилятора относительно матмодели языка, интерпретационной -- для верификации кодогенератора, трансформационной -- для верификации средств метапрограммирования или транскомпиляции и т.п. Всё это вместе и составляет первую часть той модели, о которой я говорил.
WH>Я не знаю ничего про TLS, но HTTP это же почти регулярный язык.
WH>Из того что там не регулярное:
WH>1)Прочитать число и считать количество байт равное этому числу.
И это уже делает HTTP контекстно-зависимым языком (см. https://pdfs.semanticscholar.org/7d95/6ddef192f3a10b22bc41044566be396c751f.pdf, п3.3), для разбора которого требуется LBA, суть -- машина Тьюринга с ограниченной памятью.
WH>Вот предикаты, которым должны соответствовать все сортировки. Верифицировать их нужно глазами. Благо они очень простые.
Они действительно простые, но только потому, что простыми в данном примере являются формулы определения отношения частичного порядка на множестве элементов, выступающие здесь в роли первой части упомянутой модели.
WH>//Предикат который утверждает что функция переставляет местами элементы массива [begin..end)
WH>//и не меняет остальной массив
И вот тут мы приходим ко второй части модели. Если опираться на определение понятия алгоритма из теории формальных языков (т.е. что всякий алгоритм является распознавателем какого-либо формального языка), то первая часть лишь доказывает, что верифицируемый алгоритм распознаёт полное множество слов, принадлежащих некоторому языку. Но нам также надо ещё и доказать, что этот же алгоритм не распознаёт слова, принадлежащие дополнению данного языка. Дополнение КЗ-языка является КЗ-языком -> ещё одна МТ с ограниченной памятью, отсутствие которой нужно доказать. А доказать отсутствие чего-либо в общем случае "гораздо труднее", чем наличие
Опять-таки, в случае сортировки вполне достаточно сказать "алгоритм может переставлять элементы входного массива, как ему вздумается, лишь бы на выходе всегда был упорядоченный массив", опираясь на допущение, что сортировка -- не более чем цепочка последовательных перестановок элементов некоторого множества. А как быть, даже в таком относительно простом случае, как, к примеру, режимы блочного шифрования с обратной связью, где каждый последующий блок шифротекста является результатом нетривиальных операций между промежуточным блоком и всеми или некоторыми предыдущими?
Для верификации криптографии, кстати, на практике используются специально заточенные под эту задачу DSL'и. Такие, как https://github.com/GaloisInc/cryptol, например. Просто потому, что описать даже примитивные криптоалгоритмы традиционными средствами верификации невероятно тяжело. И это при том, что за любым таким алгоритмом стоит совершенно строгая формальная модель. Что касается прочих классов уязвимостей, то частичные модели на данный момент, построены только для инъекций, некоторых подклассов атак повреждения памяти и гонок за ресурсами. Для всех остальных классов моделей нет, а значит и нет возможности верифицировать код на предмет их отсутствия.
WH>Ну и на практике нам нужно верифицировать не всё, а только некоторые свойства программы. Такие как не выход за приделы массива.
Уязвимость -- есть множество достижимых состояний приложения (конфигураций в терминологии Тьюринга), в которых для любого информационного потока нарушается любое из свойств защищённости (в общепринятой модели угроз это -- конфиденциальность, доступность, целостность, авторизованность и аутентичность). Для того, чтобы доказать безопасность приложения средствами частичной формальной верификации (т.е. когда верифицируется не всё), мы должны помимо всего прочего ещё и доказать, что верификация покрывает всё множество таких состояний. Не буду утверждать, что это неразрешимая проблема (хотя, IMO, так оно и есть), но вот то, что известных способов её решения на данный момент не существует -- совершенно точно.