Wyniki wyszukiwania - BazTech

1

Partial mathematical modeling and analysis of the AES system

Stachowiak Sylwia, Kurkowski Mirosław

Journal of Applied Mathematics and Computational Mechanics

|

2023

|

Vol. 22, nr 4

64-78

EN

Many types of decision problems can be solved using mathematical modeling and analysis. Such techniques are also developed on the border of mathematical logic and computer science. A good example is the translation of the issues examined into the Satisfiability Problem (SAT) of a logical propositional formula. Unfortunately, this method is not always practical, considering the high computational complexity of solving the SAT problem. It often happens that in the studied cases, the encoding formulas contain even hundreds of thousands of clauses and propositional variables. However, even in these cases, modern SAT solvers can sometimes successfully solve these problems. This approach can be used to cryptanalyze some symmetric ciphers or parts/modifications. In this case, the encryption algorithm is first translated into a boolean formula. Then additional formulas are created to encode randomly selected plaintext and the key bits. Using the SAT solver; we can count the values of the ciphertext bits. Then, using the SAT solver again, we proceed to the cryptanalysis of the cipher with the selected plaintext and proper ciphertext, looking for the bits of the encryption key. In this paper, we will present the new results of how SAT techniques behave against representative fragments of the AES cipher, the current standard for symmetric encryption. We also compare the results obtained in this case by several SAT solvers. In addition, we present the results of the SAT-solver CryptoMiniSat obtained during the attack on the 1st round of the AES-128 cipher.

2

An example of the satisfiability problem in the continuous structure

Balcer Marek

Silesian Journal of Pure and Applied Mathematics

|

2020

|

vol. 10, iss. 1

121--131

EN

The paper presents and demonstrates the theorem showing the equivalence of the problem of the verifiability test of a logical expression in the discrete model N of the logic with the search for the minimum value of a continuous function generated by this expression in the structure N, which is a simple extension of M. Theoretical considerations are illustrated by the example of a certain semi-heuristic algorithm seeking the minimum value of function ϕ with a short statistics of its.

3

MILP, Pseudo-Boolean, and OMT Solvers for Optimal Fault-Tolerant Placements of Relay Nodes in Mission Critical Wireless Networks

Chen Qian Matteo, Finzi Alberto, Mancini Toni, Melatti Igor, Tronci Enrico

Fundamenta Informaticae

|

2020

|

Vol. 174, nr 3/4

229--258

EN

In critical infrastructures like airports, much care has to be devoted in protecting radio communication networks from external electromagnetic interference. Protection of such mission-critical radio communication networks is usually tackled by exploiting radiogoniometers: at least three suitably deployed radiogoniometers, and a gateway gathering information from them, permit to monitor and localise sources of electromagnetic emissions that are not supposed to be present in the monitored area. Typically, radiogoniometers are connected to the gateway through relay nodes. As a result, some degree of fault-tolerance for the network of relay nodes is essential in order to offer a reliable monitoring. On the other hand, deployment of relay nodes is typically quite expensive. As a result, we have two conflicting requirements: minimise costs while guaranteeing a given fault-tolerance. In this paper, we address the problem of computing a deployment for relay nodes that minimises the overall cost while at the same time guaranteeing proper working of the network even when some of the relay nodes (up to a given maximum number) become faulty (fault-tolerance ). We show that, by means of a computation-intensive pre-processing on a HPC infrastructure, the above optimisation problem can be encoded as a 0/1 Linear Program, becoming suitable to be approached with standard Artificial Intelligence reasoners like MILP, PB-SAT, and SMT/OMT solvers. Our problem formulation enables us to present experimental results comparing the performance of these three solving technologies on a real case study of a relay node network deployment in areas of the Leonardo da Vinci Airport in Rome, Italy.

4

Satisfiability versus Finite Satisfiability in Elementary Modal Logics

Michaliszyn J., Otop J., Witkowski P.

Fundamenta Informaticae

|

2018

|

Vol. 163, nr 2

165--188

EN

We study variants of the satisfiability problem of elementary modal logics, i.e., modal logic considered over first-order definable classes of frames. The standard semantics of modal logic allows infinite structures, but often practical applications require to restrict our attention to finite structures. A number of decidability and undecidability results for the elementary modal logics were proved separately for general satisfiability and finite satisfiability. In this paper we justify that the results for both kinds of the satisfiability problem must be shown separately – we prove that there is a universal first-order formula that defines an elementary modal logic with decidable general satisfiability problem, but undecidable finite satisfiability problem, and, the other way round, that there is a universal first-order formula that defines an elementary modal logic with decidable finite satisfiability problem, but undecidable general satisfiability problem.

5

SMT-based Searching for κ-quasi-optimal Runs in Weighted Timed Automata

Woźna-Szcześniak B., Zbrzezny A. M., Zbrzezny A.

Fundamenta Informaticae

|

2017

|

Vol. 152, nr 4

411--433

EN

We investigate a quasi-optimal cost reachability problem for weighted timed automata. We use a translation to the satisfiability modulo theories (SMT) problem to solve the problem. In particular, we show how to find a run of length κ ∊ N that starts at the initial state and terminates at a state containing the target location, its total cost belongs to the interval [c; c + 1), for some natural number c ∊ IN, and the cost of each other run of length κ, which also leads from the initial state to a state containing the target location, is greater or equal to c. This kind of run is called κ-quasi-optimal. We exemplify the use of our solution to the investigated problem by means of the weighted timed generic pipeline protocol and the weighted job shop scheduling problem, and we provide some preliminary experimental results.

6

A Function Elimination Method for Checking Satisfiability of Arithmetical Logics

Castiglioni V., Lanotte R., Tini S.

Fundamenta Informaticae

|

2016

|

Vol. 143, nr 1/2

51--71

EN

We study function elimination for Arithmetical Logics. We propose a method allowing substitution of functions occurring in a given formula with functions with less arity. We prove the correctness of the method and we use it to show the decidability of the satisfiability problem for two classes of formulas allowing linear and polynomial terms.

7

A parallel pipelined naive method for testing satisfiability

Sadowski A., Jakubski A., Michalski G.

Przegląd Elektrotechniczny

|

2015

|

R. 91, nr 11

154-157

EN

Field Programmable Gate Array (FPGA) systems are highly suitable for solving satisfiability problems SAT. The paper will present the possibilities in programmable FPGA chips to test satisfiability by use of parallelism and pipelining. There will be presented various options to approach this problem by use of VHDL language. For this purpose, authors created a dedicated architecture, combined with a PC, by use of the UART protocol. To build the architecture authors used a Xilinx Spartan-3AN plate, the synthesis was performed in the ISE 11.3. Xilinx software.

PL

Układy FPGA ze względu na swoją architekturę bardzo dobrze pasują do rozwiązywania zagadnień z zakresu rozwiązywania problemów spełnialności SAT. W artykule przedstawiono współbierzne rozwiązanie problemu spełnialności z zastosowaniem programowalnych układów FPGA. Dla potrzeb realizacji zadania opracowno dedykowaną architekturę, opartą o układ FPGA (Xilinx Spartan-3AN) komunikującą się za pomocą protokołu UART.

8

Akceleracja obliczeń kryptograficznych z wykorzystaniem procesorów GPU

Bęza P., Gocławski J., Mral P., Sapiecha P.

Studia Bezpieczeństwa Narodowego

|

2014

|

R. 4, Nr 6

341--357

PL

Problem spełnialności formuł rachunku zdań SAT jest jednym z fundamentalnych oraz otwartych zadań we współczesnej informatyce. Jest on problemem NP-zupełnym. To znaczy, że wszystkie problemy z klasy NP możemy sprowadzić do problemu SAT w czasie wielomianowym. Co ciekawe, wśród problemów z klasy NP istnieje wiele takich, które są ściśle związanych z kryptologią, na przykład: faktoryzacja liczb – ważna dla RSA, łamanie kluczy szyfrów symetrycznych, znajdowanie kolizji funkcji skrótu i wiele innych. Odkrycie wielomianowego algorytmu dla SAT skutkowałoby rozwiązaniem problemu milenijnego: P vs. NP. Cel ten wydaje się bardzo trudny do osiągnięcia – nie wiadomo nawet czy jest możliwy. Mając nieco mniejsze aspiracje możemy projektować algorytmy heurystyczne lub losowe dla SAT. W związku z tym, głównym celem autorów pracy jest przedstawienie projektu równoległego SAT Solvera bazującego na algorytmie WalkSAT, w tym procesu jego implementacji z wykorzystaniem środowiska programistycznego OpenCL oraz komputera wyposażonego w karty graﬁczne NVIDIA Tesla. Wraz z dynamicznym rozwojem technologii procesorów typu GPU oraz układów FPGA, jak również przenośnością rozwiązań stworzonych w Open CL, kierunek takich prac staje się interesujący ze względu na uzyskiwaną efektywność obliczeniową, jak również szybkość prototypowania rozwiązań.

EN

The Boolean satisﬁability problem SAT is one of the fundamental and open tasks in present-day information science. This problem is NP-complete. It means that all NP problems can be reduced to SAT in polynomial time. Interestingly, among NP problems, there are many closely related to cryptology, for example: factorization of numbers – important for RSA, breaking keys of symmetric ciphers, ﬁnding collisions of hash functions and many others. The discovery of the polynomial algorithm for SAT would result in resolving one of Millennium Prize Problems: P vs. NP. This objective seems to be hard to achieve – it’s unknown if it is even possible. With slightly lower aspirations, we can design heuristic or random algorithms for SAT. Therefore, the main goal of our study is to present a project of parallel SAT Solver based on WalkSAT algorithm, including its implementation using the OpenCL programming environment and a computer equipped with NVIDIA Tesla graphics cards. With the rapid development of GPU technology and FPGAs, as well as portability of solutions created in OpenCL, the direction of such works becomes interesting because of computational eﬃciency gained, as well as solution prototyping rate.

9

SMT-Based Reachability Checking for Bounded Time Petri Nets

Półrola A., Cybula P., Męski A.

Fundamenta Informaticae

|

2014

|

Vol. 135, nr 4

467--482

EN

Time Petri nets by Merlin and Farber are a powerful modelling formalism. However, symbolic model checking methods for them consider in most cases the nets which are 1-safe, i.e., allow the places to contain at most one token. In our paper we present an approach which applies symbolic verification to testing reachability for time Petri nets without this restriction. We deal with the class of bounded nets restricted to disallow multiple enabledness of transitions, and present the method of reachability testing based on a translation into a satisfiability modulo theory (SMT).

10

Can Machine Learning Learn a Decision Oracle for NP Problems? A Test on SAT

Grozea C., Popescu M.

Fundamenta Informaticae

|

2014

|

Vol. 131, nr 3-4

441--450

EN

This note describes our experiments aiming to empirically test the ability of machine learning models to act as decision oracles for NP problems. Focusing on satisfiability testing problems, we have generated random 3-SAT instances and found out that the correct branch prediction accuracy reached levels in excess of 99%. The branching in a simple backtracking-based SAT solver has been reduced in more than 90% of the tested cases, and the average number of branching steps has reduced to between 1/5 and 1/3 of the one without the machine learning model. The percentage of SAT instances where the machine learned heuristic-enhanced algorithm solved SAT in a single pass reached levels of 80-90%, depending on the set of features used.

11

On the Satisfiability Problem for a 4-level Quantified Syllogistic and Some Applications to Modal Logic

Cantone D., Asmundo M. N.

Fundamenta Informaticae

|

2013

|

Vol. 124, nr 4

427--448

EN

We introduce a multi-sorted stratified syllogistic, called 4LQSR, admitting variables of four sorts and a restricted form of quantification over variables of the first three sorts, and prove that it has a solvable satisfiability problem by showing that it enjoys a small model property. Then, we consider the fragments (4LQSR)h of 4LQSR, consisting of 4LQSR-formulae whose quantifier prefixes have length bounded by h ≥⃒ 2 and satisfying certain additional syntactical constraints, and prove that each of them has an NP-complete satisfiability problem. Finally we show that the modal logic K45 can be expressed in (4LQSR)3.

12

Better Algorithms for Satisfiability Problems for Formulas of Bounded Rank-width

Ganian R., Hlinĕný P., Obdržálek J.

Fundamenta Informaticae

|

2013

|

Vol. 123, nr 1

59--76

EN

We provide a parameterized algorithm for the propositional model counting problem #SAT, the runtime of which has a single-exponential dependency on the rank-width of the signed graph of a formula. That is, our algorithm runs in time O(t3 · 23t(t+1)/2 ·|φ| for a width-t rankdecomposition of the input φ, and can be of practical interest for small values of rank-width. Previously, analogical algorithms have been known – e.g. [Fischer, Makowsky, and Ravve] – with a single-exponential dependency on the clique-width k of the signed graph of a formula with a given k-expression. Our algorithm presents an exponential runtime improvement over the worst-case scenario of the previous one, since clique-width reaches up to exponentially higher values than rankwidth. We also provide an algorithm for the MAX-SAT problem along the same lines.

13

Constraint Satisfaction Problems in Clausal Form II: Minimal Unsatisfiability and Conflict Structure

Kullmann O.

Fundamenta Informaticae

|

2011

|

Vol. 109, nr 1

83-119

EN

Concluding this mini-series of 2 articles on the foundations of generalised clause-sets, we study the combinatorial properties of non-boolean conjunctive normal forms (clause-sets), allowing arbitrary (but finite) sets of values for variables, while literals express that some variable shall not get some (given) value. First we study the properties of the direct translation (or "encoding") of generalised clause-sets into boolean clause-sets. Many combinatorial properties are preserved, and as a result we can lift fixed-parameter tractability of satisfiability in the maximal deficiency from the boolean case to the general case. Then we turn to irredundant clause-sets, which generalise minimally unsatisfiable clause-sets, and we prove basic properties. The simplest irredundant clause-sets are hitting clause-sets, and we provide characterisations and generalisations. Unsatisfiable irredundant clause-sets are the minimally unsatisfiable clause-sets, and we provide basic tools. These tools allow us to characterise the minimally unsatisfiable clause-sets of minimal deficiency. Finally we provide a new translation of generalised boolean clause-sets into boolean clause-sets, the nested translation, which preserves the conflict structure. As an application, we can generalise results for boolean clause-sets regarding the hermitian rank/defect, especially the characterisation of unsatisfiable hitting clause-sets where between every two clauses we have exactly one conflict. We conclude with a list of open problems, and a discussion of the "generic translation scheme".

14

SAT as a Programming Environment for Linear Algebra

Srebrny M., Stępień L.

Fundamenta Informaticae

|

2010

|

Vol. 102, nr 1

115-127

EN

In this paper we pursue the propositional calculus and the SATisfiability solvers as a powerful declarative programming environment that makes it possible to create and run the propositional declarative programs for computational tasks in various areas of mathematics. We report some experimental results on our application of the propositional SATisfiability environment to computing some simple orthogonal matrices and the orders of some orthogonal groups. Some encouraging (and not very encouraging) experiments are reported for the proposed propositional search procedures using off-the-shelf general-purpose SAT solvers. Our new software toolkit SAT4Alg is announced.

15

Logic, primes and computation: a tale of unrest

Leonesi S., Toffalori C.

TASK Quarterly : scientific bulletin of Academic Computer Centre in Gdansk

|

2005

|

Vol. 9, No 3

273-291

EN

The early connections between Mathematical Logic and Computer Science date back to the thirties and to the birth itself of modern Theoretical Computer Science, and concern computability. This survey wishes to emphasize how alive and fruitful this relationship has been since then, and still is.