Znalezienie półcienia problemu satysfakcji z ograniczeń

Podczas testowania bezpieczeństwa systemu lub modelu wielokrotnie pojawiło się następujące pytanie .

Motywacja: Wady bezpieczeństwa oprogramowania często nie wynikają z błędów spowodowanych prawidłowymi danymi wejściowymi, ale z błędów wynikających z nieprawidłowych danych wejściowych, które są wystarczająco zbliżone do prawidłowych danych wejściowych, aby przejść przez wiele prostych kontroli poprawności. Klasycznym przykładem jest oczywiście przepełnienie bufora, w którym dane wejściowe są uzasadnione, z wyjątkiem tego, że są zbyt duże. Kompilatory i inne narzędzia mogą pomóc rozwiązać te problemy, modyfikując układ stosu i sterty oraz innymi technikami zaciemniania. Alternatywą jest usunięcie problemów z samego kodu źródłowego. Jedna technika zwana fuzzingiem bombarduje program z wejściami zbliżonymi do oczekiwanych, ale w niektórych miejscach są nieuzasadnione (duże wartości dla liczb całkowitych lub ciągów znaków). Chciałbym zrozumieć rozmycie (jako przykład) z bardziej formalnej perspektywy.

Załóżmy, że przestrzeń prawidłowych danych wejściowych jest opisana przez ograniczenia . Niech będzie zbiorem rozwiązań takich ograniczeń, a mianowicie , gdzie jest przestrzenią możliwych danych wejściowych. $\Phi$ $M$ $M=\lbrace m\in\mathcal{M}~|~m\models\Phi\rbrace$ $\mathcal{M}$

Szukam pracy opisującej następujące pojęcia:

Półcień z jest zbiorem taki, że dla każdego i w pewnym sensie elementy są blisko elementów . Można myśleć o półcieniu jako prawie rozwiązaniu . Oczywiście to pojęcie nie będzie unikalne. $M$ $M'\subseteq \mathcal{M}$ $m\in M'$ $m\not\models\Phi$ $M'$ $M$
$\Phi$ $\Phi'$ $\Phi\Rightarrow\Phi'$ $\Phi'\land\neg\Phi$ $\Phi$

„Penumbra” to słowo, które wybrałem, aby opisać tę koncepcję. Można to nazwać czymś innym.

Inspirację znalazłem w morfologii matematycznej , stąd moja metafora wizualna, ale oba światy są od siebie oddzielone. Czy jest tam jakaś przydatna praca? A może w świecie surowych zestawów ?

Czy ktoś może rzucić światło?

lo.logic csp security

— Dave Clarke
źródło

Problem sam w sobie jest naprawdę interesujący, jednak w większości przypadków zainteresowanie nie budowaniem półcieni (nie znam bardziej „oficjalnej” nazwy), ale raczej zaciemnianiem technik, które pozwalają uniknąć ataków oprogramowania (takich jak ataki poprzez modyfikację) wejścia). Techniki te ukrywają rdzeń zachowania programu, zalewając go czymś innym. Na przykład, możesz zbudować program, przeplatając oryginalny wraz z programem, który koduje na stałe rozwiązanie problemu NP na konkretnej instancji.

— Sylvain Peyronnet,

To prawda. Nawiązuję do podejścia znanego jako fuzzing.

— Dave Clarke

Nawiasem mówiąc, CSP = Problem Satysfakcji Ograniczenia.

— MS Dousti

Wiele uwagi poświęconej wariantom optymalizacji problemu ograniczenia ograniczeń (CSP) koncentrowało się na spełnieniu pewnej liczby ograniczeń (MAX-CSP) lub w przypadku logicznego wyboru rozwiązania, które przypisuje możliwie jak najwięcej zmiennych wartość 1 ( MAX-ONES, są też MIN-ONES).

Zamiast tego pytasz o wariant, który można by nazwać MAKSYMALNYM CZĘŚCIOWYM CSP. Zostało to zbadane przynajmniej w późnych latach sześćdziesiątych, ale nie jestem świadomy tego, że ma ustaloną nazwę. Jest to naturalny problem i dobrze byłoby zobaczyć więcej pracy nad jego badaniem. Dziękujemy za udostępnienie kolejnej potencjalnej aplikacji dla tego problemu!

Ambler, AP i Barrow, HG i Brown, CM i Burstall, RM i Popplestone, RJ, A wszechstronny system do montażu sterowanego komputerowo , Artificial Intelligence 6 129–156, 1975. doi: 10.1016 / 0004-3702 (75) 90006- 5

Zestaw przypisań zmiennych wartości nazywany jest przypisaniem częściowym . Przypisanie zmiennej wartości można napisać jako krotkę (zmienna, wartość). Częściowe przypisania są wtedy po prostu funkcjami od zmiennych do wartości. Rekwizyty to częściowe zadania, które nie naruszają żadnych ograniczeń. Odpowiednio, rekwizyt nie zawiera częściowego przypisania zabronionego przez niektóre ograniczenia (jako podzbiór).

Jednym ze sposobów wyrażenia problemu optymalizacji jest:

$f$
$|f|$

$n$ $n$ $n-1$

$k$ $d$ $k-d$

Druga część twojego pytania również wydaje się bardzo interesująca, ale nie jestem świadoma żadnej pracy z tym związanej.

Przypis: Termin rekwizyt pochodzi z mojej tezy; ma na celu przekazanie idei, że takie częściowe zadania są właściwe, a także że wspierają one zestaw rozwiązań. Jest to sprzeczne z nogood , który jest przyjętym terminem opisującym częściowe przypisanie, którego nie można rozszerzyć na rozwiązanie. Słowo „nogood” zostało wprowadzone przez Richarda Stallmana i Geralda Sussmana w 1976 r., Kiedy RMS nadal był badaczem sztucznej inteligencji zamiast aktywistą wolności oprogramowania.

Stallman, Richard M. i Sussman, Gerald Jay, Forward Reasoning and Directed-Backtracking in a System for Computer-Aided Circuit Analysis , MIT Artificial Intelligence Laboratory Memo No. 380, 1976. ( PDF )

— András Salamon
źródło