Trouver la pénombre d'un problème de satisfaction de contraintes

La question suivante s'est posée à plusieurs reprises lors du test de la sécurité d'un système ou d'un modèle.

Motivation: les failles de sécurité logicielles ne proviennent souvent pas de bogues dus à des entrées valides, mais de bogues résultant d'entrées non valides suffisamment proches des entrées valides pour passer outre la plupart des vérifications de validité simples. L'exemple classique est bien sûr les débordements de tampon, où l'entrée est raisonnable, sauf qu'elle est trop grande. Les compilateurs et autres outils peuvent aider à résoudre ces problèmes en modifiant la disposition de la pile et du tas et par d'autres techniques d'obscurcissement. Une alternative consiste à supprimer les problèmes du code source lui-même. Une technique appelée fuzzing bombarde le programme avec des entrées est proche des entrées attendues, mais est à certains endroits déraisonnable (grandes valeurs pour les champs entiers ou chaîne). J'aimerais comprendre le fuzzing (comme un exemple) d'un point de vue plus formel.

Supposons que l'espace des entrées valides soit décrit par les contraintes $\Phi$ . Soit $M$ l'ensemble des solutions de telles contraintes, à savoir $M=\lbrace m\in\mathcal{M}~|~m\models\Phi\rbrace$ , où $\mathcal{M}$ est l'espace des entrées possibles.

Je recherche un travail décrivant les notions suivantes:

• $M$$M'\subseteq \mathcal{M}$$m\in M'$ $m\not\models\Phi$ $M'$$M$

• Moyens de relâcher les contraintes à telles que premièrement et est, en un sens, la pénombre syntaxique de .$\Phi$$\Phi'$$\Phi\Rightarrow\Phi'$$\Phi'\land\neg\Phi$$\Phi$

"Penumbra" est un mot que j'ai choisi pour décrire le concept. Cela pourrait bien s'appeler autre chose.

J'ai trouvé l'inspiration dans la morphologie mathématique , d'où ma métaphore visuelle, mais les deux mondes sont séparés parsecs. Y a-t-il un travail utile là-bas? Ou peut-être dans le monde des décors rugueux ?

Quelqu'un peut-il faire la lumière?

Une grande partie de l'attention portée aux variantes d'optimisation du problème de satisfaction des contraintes (CSP) s'est concentrée sur la satisfaction d'un certain nombre de contraintes (MAX-CSP), ou dans le cas booléen sur le choix de la solution qui affecte autant de variables que possible la valeur 1 ( MAX-ONES, il y a aussi MIN-ONES).

Au lieu de cela, vous demandez une variante qui pourrait s'appeler MAXIMUM PARTIAL CSP. Cela a été étudié au moins à la fin des années 1960, mais je ne suis pas au courant qu'il ait un nom établi. C'est un problème naturel, et il serait bon de voir plus de travail pour l'étudier. Merci d'avoir fourni une autre application potentielle pour ce problème!

• Ambler, AP et Barrow, HG et Brown, CM et Burstall, RM et Popplestone, RJ, Un système polyvalent pour l'assemblage contrôlé par ordinateur , Intelligence artificielle 6 129–156, 1975. doi: 10.1016 / 0004-3702 (75) 90006- 5

Un ensemble d'affectations à valeur variable est appelé affectation partielle . On peut écrire une affectation de valeur variable comme un tuple (variable, valeur). Les affectations partielles sont alors simplement des fonctions des variables aux valeurs. Les accessoires sont des affectations partielles qui ne violent aucune contrainte. De manière équivalente, un accessoire ne contient aucune affectation partielle interdite par une contrainte (en tant que sous-ensemble).

Une façon d'exprimer le problème d'optimisation est la suivante.

CSP PARTIEL MAXIMUM:
Entrée: instance CSP
Sortie: prop Critère: maximiser$f$
$|f|$

Dans un cas avec variables, un accessoire de cardinalité sera clairement une solution. Il peut exister de grands accessoires, avec une cardinalité jusqu'à , qui ne sont contenus dans aucune solution.$n$$n$$n-1$

Dans la terminologie que vous proposez, l'ensemble des accessoires avec une cardinalité maximale forme la pénombre, peut-être même avec une marge de manœuvre supplémentaire (donc une cardinalité d'au moins ).$k$$d$$k-d$

La deuxième partie de votre question semble également très intéressante, mais je ne connais aucun travail y relatif.

Footnote: Le terme prop vient de ma thèse; il est destiné à transmettre l'idée que de telles affectations partielles sont appropriées, et qu'elles soutiennent également l'ensemble des solutions. Cela contraste avec un nogood , qui est le terme accepté pour décrire une affectation partielle qui ne peut pas être étendue à une solution. Le mot «nogood» a été introduit par Richard Stallman et Gerald Sussman en 1976, lorsque RMS était encore un chercheur en IA au lieu d'un activiste de la liberté logicielle.

• Stallman, Richard M. et Sussman, Gerald Jay, Raisonnement avant et retour en arrière dirigé par la dépendance dans un système d'analyse de circuits assistée par ordinateur , MIT Artificial Intelligence Laboratory Memo No. 380, 1976. ( PDF )