I det här dokumentet studerar vi problemet med att automatiskt kontrollera överordnad maskering av motåtgärder. Detta problem är viktigt i praktiken (svagheter har upptäckts i system som ansågs säkra), men är i sig exponentiellt: för t-order maskering innebär det att bevisa att varje delmängd av t mellanliggande variabler distribueras oberoende av hemligheterna. Vissa typer av system har föreslagits för att hjälpa kryptografer att kontrollera sina bevis, men många av dessa metoder är otillräckliga för att genomföra högre ordning. Vi föreslår en ny metod, baserad på programverifieringstekniker, för att kontrollera oberoendet av uppsättningar av intermediära variabler från vissa hemligheter. Vår nya språkbaserade karakterisering av problemet gör också att vi kan utforma och genomföra flera algoritmer som kraftigt minskar antalet uppsättningar av variabler som måste övervägas för att bevisa denna självständighet egenskap på alla giltiga motståndare observationer. Resultatet av dessa algoritmer är antingen ett bevis på säkerhet eller en uppsättning observationer där självständighetsfastigheten inte kan bevisas. Vi fokuserar på AES implementeringar för att kontrollera giltigheten av våra algoritmer. Vi bekräftar också verktygets förmåga att ge användbar information när bevisen misslyckas, genom att återupptäcka befintliga attacker och upptäcka nya.
Barthe m.fl. I REF föreslogs en relationsanalysteknik för att kontrollera att högordermaskering var korrekt.
Verified Proofs of Higher-Order Masking
{'venue': 'IACR Cryptology ePrint Archive', 'journal': 'IACR Cryptology ePrint Archive', 'mag_field_of_study': ['Computer Science', 'Mathematics']}