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

  Modern competitive solvers employ various preprocessing techniques to efficiently tackle complex problems. This work introduces two preprocessing techniques to improve solving weighted partial MaxSAT problems: Generalized Boolean Multilevel Optimization (GBMO) and Trimming MaxSAT (TrimMaxSAT). GBMO refines and extends Boolean Multilevel Optimization (BMO), thereby splitting instances due to their distribution of weights into multiple less complex subproblems, which are solved one after the other to obtain the overall solution. The second technique, TrimMaxSAT, finds unsatisfiable soft clauses and removes them from the instance. This reduces the complexity of the MaxSAT instance and works especially well in combination with GBMO. The proposed algorithm works incrementally in a binary search fashion, testing the satisfiability of every soft clause. Furthermore, as a by-product, typically an initial weight close to the maximum is found, which is in turn advantageous w.r.t. the size of e.g. the Dynamic Polynomial Watchdog (DPW) encoding. 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

  In this paper we present a novel pseudo-Boolean (PB) constraint encoding for solving the weighted MaxSAT problem with iterative SAT-based methods based on the Polynomial Watchdog (PW) CNF encoding. The watchdog of the PW encoding indicates whether the bound of the PB constraint holds. In our approach, we lift this static watchdog concept to a dynamic one allowing an incremental convergence to the optimal result. Consequently, we formulate and implement a SAT-based algorithm for our new Dynamic Polynomial Watchdog (DPW) encoding which can be applied for solving the MaxSAT problem. Furthermore, we introduce three fundamental optimizations of the PW encoding also suited for the original version leading to significantly less encoding size. 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.