2021

 nach oben zur Jahresübersicht

• Tobias Paxian, Pascal Raiola, Bernd Becker
  On Preprocessing for Weighted MaxSAT
  2021 VMCAI - 22nd International Conference on Verification, Model Checking, and Abstract Interpretation, Springer, Band: 12597, Seiten: 556 - 577
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Both techniques can be used by all MaxSAT solvers, though our focus lies on Pseudo Boolean constraint based MaxSAT solvers. Experimental results show the effectiveness of both techniques on a large set of benchmarks from a hardware security application and from the 2019 MaxSAT Evaluation. In particular for the hardest of the application benchmarks, the solver Pacose with GBMO and TrimMaxSAT performs best compared to the MaxSAT Evaluation solvers of 2019. For the benchmarks of the 2019 MaxSAT Evaluation, we show that with the proposed techniques the top solver combination solves significantly more instances.

2020

 nach oben zur Jahresübersicht

• Pascal Raiola, Tobias Paxian, Bernd Becker
  Minimal Witnesses for Security Weaknesses in Reconfigurable Scan Networks
  2020 IEEE European Test Symposium
• Tobias Paxian, Bernd Becker
  Pacose: an iterative SAT-based MaxSAT solver
  2020 MaxSAT Evaluation 2020: Solver and Benchmark Descriptions, Band: 16, Seiten: 12 - 12
• Pascal Raiola, Tobias Paxian, Bernd Becker
  Partial (un-) weighted MaxSAT benchmarks: minimizing witnesses for security weaknesses in reconfigurable scan networks
  2020 MaxSAT Evaluation 2020, Band: 14, Seiten: 44 - 44
• Tobias Paxian, Mael Gay, Devanshi Upadhyaya, Bernd Becker, Ilia Polian
  SAT Benchmarks of AutoFault Attacking AES, LED and PRESENT
  2020 SAT COMPETITION 2020, Band: 20, Seiten: 79 - 79

2019

 nach oben zur Jahresübersicht

• Ilia Polian, Mael Gay, Tobias Paxian, Sauer Matthias, Bernd Becker
  Automatic construction of fault attacks on cryptographic hardware implementations
  2019 Automated Methods in Cryptographic Fault Analysis, Band: 1, Seiten: 151 - 170
• Mael Gay, Tobias Paxian, Devanshi Upadhyaya, Bernd Becker, Ilia Polian
  Hardware-oriented algebraic fault attack framework with multiple fault injection support
  2019 2019 Workshop on Fault Diagnosis and Tolerance in Cryptography (FDTC), Band: 16, Seiten: 25 - 32
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  The evaluation of fault attacks on security-critical hardware implementations of cryptographic primitives is an important concern. In such regards, we have created a framework for automated construction of fault attacks on hardware realization of ciphers. The framework can be used to quickly evaluate any cipher implementations, including any optimisations. It takes the circuit description of the cipher and the fault model as input. The output of the framework is a set of algebraic equations, such as conjunctive normal form (CNF) clauses, which is then fed to a SAT solver. We consider both attacking an actual implementation of a cipher on an field-programmable gate array (FPGA) platform using a fault injector and the evaluation of an early design of the cipher using idealized fault models. We report the successful application of our hardware-oriented framework to a collection of ciphers, including the advanced encryption standard (AES), and the lightweight block ciphers LED and PRESENT. The corresponding results and a discussion of the impact to different fault models on our framework are shown. Moreover, we report significant improvements compared to similar frameworks, such as speedups or more advanced features. Our framework is the first algebraic fault attack (AFA) tool to evaluate the state-of-the art cipher LED-64, PRESENT and full-scale AES using only hardware-oriented structural cipher descriptions.

2018

 nach oben zur Jahresübersicht

• Tobias Paxian, Sven Reimer, Bernd Becker
  Dynamic Polynomial Watchdog Encoding for Solving Weighted MaxSAT
  2018 International Conference on Theory and Applications of Satisfiability Testing, Springer, Band: 10929, Seiten: 37 - 53
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Our experimental results show that our encoding and algorithm is competitive with state-of-the-art encodings as utilized in QMaxSAT (2nd place in last MaxSAT Evaluation 2017). Our encoding dominates two of the QMaxSAT encodings, and at the same time is able to solve unique instances. We integrated our new encoding into QMaxSAT and adapt the heuristic to choose between the only remaining encoding of QMaxSAT and our approach. This combined version solves 19 (4%) more instances in overall 30\% less run time on the benchmark set of the MaxSAT Evaluation 2017. Compared to each encoding of QMaxSAT used in the evaluation, our encoding leads to an algorithm that is on average at least 2X faster.