ASMXperience

RESSOURCES / VOCABULAIRE

Remonter aux sources.

Des références primaires pour vérifier les concepts. Les propriétés spécifiques du moteur sont documentées à partir de son implémentation locale.

01

Synthèse guidée par contre-exemples ↗

Armando Solar-Lezama — cours de synthèse, MIT

Comprendre la boucle proposition, contre-exemple, raffinement. Perspective du projet, pas une fonctionnalité déjà intégrée.

02

Stochastic Superoptimization ↗

Eric Schkufza, Rahul Sharma, Alex Aiken — ASPLOS 2013

Article de recherche primaire sur la recherche stochastique de programmes binaires sans boucle. Les résultats de STOKE ne sont pas ceux d’ASMXperience.

03

FixedSizeBitVectors ↗

SMT-LIB — théorie des vecteurs de bits

Sémantique formelle pour modéliser les mots de largeur finie. Adapter explicitement les décalages aux règles du langage candidat.

04

Instruction set reference ↗

Intel — Software Developer’s Manuals

Référence officielle des instructions, registres et effets machine. Consulter la variante et la largeur effectivement encodées.

06

VirtualProtect ↗

Microsoft Learn — Win32

Contrat de changement des protections des pages engagées.

08

Sandboxie : commandes de lancement ↗

Documentation du projet Sandboxie-Plus

Sélection d’un bac, lancement et contrôle des processus. Une commande réussie ne constitue pas à elle seule un test complet de confinement.

LEXIQUE

Des termes, des contrats précis.

ABI
Contrat entre appelant et appelé : passage des arguments, registres à préserver, pile et valeur de retour.
Bloat
Croissance de la taille des programmes sans amélioration proportionnelle du comportement ou du coût.
Candidat
Programme proposé par le moteur. Son existence ne signifie ni correction ni nouveauté.
CEGIS
Counterexample-Guided Inductive Synthesis : boucle de synthèse et vérification alimentée par les entrées réfutantes.
Checkpoint
État sauvegardé permettant de reprendre la population et le générateur pseudo-aléatoire.
Distance de Hamming
Nombre de positions binaires différentes entre deux mots de même longueur.
Élite
Meilleur membre conservé lors du remplacement ; le critère actuel privilégie le score, puis la brièveté en cas d’égalité.
Fitness
Mesure utilisée pour orienter la sélection. Elle n’est pas nécessairement égale au but scientifique final.
Génome
Représentation syntaxique d’un programme : ici une suite bornée de couples opération/immédiat.
Intron
Fragment qui ne modifie pas le comportement observé dans le contexte étudié.
Oracle
Référence utilisée pour produire ou vérifier la réponse attendue. Un oracle erroné peut guider une recherche erronée.
Pareto
Notion de dominance pour plusieurs objectifs : améliorer un critère sans dégrader les autres.
PRNG
Générateur pseudo-aléatoire déterministe une fois sa graine et son état fixés.
Ring 3
Mode utilisateur du processeur. Il ne définit pas à lui seul une politique d’accès aux fichiers.
SAT / UNSAT
Satisfiable / insatisfiable pour une formule et une théorie données. UNKNOWN n’est ni l’un ni l’autre.
Sémantique
Signification comportementale d’un programme, par opposition à sa seule représentation textuelle ou binaire.
SSE
Server-Sent Events : flux HTTP persistant permettant au serveur d’envoyer des événements au navigateur.
Surapprentissage
Adaptation aux tests consultés qui ne se traduit pas nécessairement par une généralisation.
W^X
Discipline évitant qu’une même page soit simultanément inscriptible et exécutable.