Nous présentons une méthode originale de recherche de preuve par récurrence utilisant la surréduction. Elle a la particularité d'être fondée sur la déduction modulo et d'utiliser la surréduction pour sélectionner à la fois les variables de récurrence et les schémas d'instanciation. Elle donne également la possibilité de traduire directement toute dérivation effectuée avec succès en une preuve dans le calcul des séquents modulo. La correction et la complétude réfutationnelle de la méthode sont démontrées en théorie de la preuve. Nous étendons ensuite cette première approche aux théories de réécriture équationnelles constituées d'un système de réécriture R et d'un ensemble E d'égalités. A partir du moment où le système de réécriture équationnel (R,E) possède de bonnes propriétés de terminaison et de complétude suffisante, et si on suppose également que E préserve les constructeurs, la surréduction au niveau des positions les plus profondes où apparaît un symbole défini s'effectue uniquement à l'aide d'unificateurs qui sont également des substitutions constructeurs. Ceci est particulièrement intéressant dans le cas des théories associatives, ou associatives commutatives, pour lesquelles notre système de recherche de preuve a été raffiné. / We are presenting an original narrowing-based proof search method for inductive theorems. It has the specificity to be grounded on deduction modulo and to rely on narrowing to provide both induction variables and instantiation schemes. It also yields a direct translation from a successful proof search derivation to a proof in the sequent calculus. The method is shown to be correct and refutationally complete in a proof theoretical way. We are extending this first approach to equational rewrite theories given by a rewrite system R and a set E of equalities. Whenever the equational rewrite system (R,E) has good properties of termination, sufficient completeness, and whenever E is constructor preserving, narrowing at defined-innermost positions is performed with unifiers which are constructor substitutions. This is especially interesting for associative and associative-commutative theories for which the general proof search system is refined.

Cette thèse est constituée de deux parties indépendantes, étudiant deux aspects de la théorie des (φ,Γ)-modules en caractéristique p. La première partie porte sur l'étude de la réduction modulo p des représentations cristallines irréductibles de dimension deux. Nous donnons, pour des poids k ≤ p², un calcul explicite de la réduction de V(k,a) pour a dans un disque fermé centré en zéro, généralisant ainsi des résultats déjà connus pour k ≤ 2p. En particulier, nous calculons le plus grand rayon possible pour ce disque, et montrons que dans certains cas, la réduction qui est constante à l'intérieur du disque change sur son bord. Dans la seconde partie, nous nous intéressons aux représentations d'un sous-groupe de Borel de GL[indice]2(Q[indice]p) sur un corps de caractéristique p, et en particulier à celles qui sont lisses, irréductibles et admettent un caractère central. Une méthode pour construire de telles représentations à partir de (φ,Γ)-modules irréductibles a été décrite par Colmez dans sa construction de la correspondance de Langlands p-adique. Après avoir donné un cadre un peu plus général dans lequel la construction de Colmez fonctionne encore, nous classifions les représentations irréductibles du Borel, prouvant que la construction précédente permet d'obtenir toutes les représentations de dimension infinie. Lorsque le corps des coefficients est fini, ou algébriquement clos, nous disposons d'une interprétation galoisienne des (φ,Γ)-modules irréductibles, et la classification précédente permet alors d'obtenir une correspondance entre ces représentations du Borel et des représentations galoisiennes modulaires. / This thesis is made of two independent parts, dealing with two different aspects of characteristic p (φ,Γ)-modules. In the first part we study the reduction modulo p of -2-dimensional irreducible crystalline representations. For weights k ≤ p2, we give an explicit description of the reduction V(k,a) for a belonging to a closed disk centered at zero, generalizing results already known for k ≤ 2p. We explicitely compute the biggest possible radius for this disk, and prove that in some cases, the reduction which is constant on the interior of the disk is different for a belonging to the border of the disk. In the second part, we study the smooth, irreducible representations of a Borel subgroup of GL[indice]2(Q[indice]p) over a field of characteristic p and admitting a central character. One way of constructing such representations from irreducible (φ,Γ)-modules was described by Colmez in his construction of the p-adic Langlands correspondence. After giving a more general framework for Colmez's construction, we classify the irreducible representations of the Borel subgroup, proving that the previous construction already gives all the infinite dimensional representations. When the coefficient field is finite, Fontaine's equivalence combined with the previous classification gives a correspondence between these representations of a Borel subgroup of GL[indice]2(Q[indice]p) and modular galois representations.

Title: Attacks based on hardware bugs Author: Martina Válková Department: Department of Algebra Supervisor: Mgr. Štěpán Holub, Ph.D. Supervisor's e-mail address: Stepan.Holub@mff.cuni.cz Abstract: The study concerns hardware bugs producing computational errors and cryptanalytic attacks which utilize them. Particularly, the research is focused on attacks presented in the article by Biham E., Carmeli Y., Shamir A.: Bug Attacks [1] and their practical application in the case of schemes RSA and Pohlig-Hellman and various computational circumstances, which points out bigger vulnerability of schemes in the case of using the Right- to-Left modular exponentiation algorithm. The attacks have been tested against the software simulation of a faulty processor, which confirmed that they pose a real security threat in point of that situation. The mathematical part of this work concerns the problem of the finding any roots in Zp. Keywords: hardware bug, attack, RSA, roots modulo p

L'analyse statique est utilisée pour vérifier de manière formelle qu'un programme ne fait pas d'erreurs, mais un analyseur statique est lui même un programme complexe sujet aux erreurs. Une analyse statique formalisée comme un interpreteur abstrait peut être prouvée correcte, cependant un telle preuve ne porte pas directement sur l'implementation de l'analyseur. Pour résoudre cette difficultée, nous proposons de générer des conditions de vérification (VCs, des formules logiques valides seulement si le résultat de l'analyseur est correct), et de les décharger à l'aide d'un prouveur de théorèmes automatique (ATP). Les VCs générées appartiennent à la logic du premier ordre multi-sortée (MSFOL), une logique utilisée avec succés en vérification déductive, suffisament expressive pour encoder les résultats d'analyses complexes et pour formaliser la sémantique operationnelle d'un langage objet, ce qui nous permet de prouver la correction des VCs générées à l'aide d'outils de vérification deductive. Pour assurer que les VCs puissent être déchargée automatiquement pour des analyses du tas, nous introduisons un calcul de VCs appartenant à un fragment décidable de MSFOL, et afin de pouvoir utiliser le même calcul pour différentes analyses, nous décrivons une famille d'analyses à l'aide d'une fonction de concretisation et d'un instrumentation de la sémantique paramétrées. Pour améliorer la fiabilité des ATPs, nous étudions aussi la certification de résultat des proveurs de satisfiabilité modulo théories, une famille d'ATPs dédiée à MSFOL. Nous proposons un système de preuve et un vérifieur modulaires, qui s'appuient sur des vérifieur dédiés aux théories sous-jacentes. / Static program analysis is a core technology for both verifying and finding errors in programs but most static analyzers are complex pieces of software that are not without error. A Static analysis formalised as an abstract interpreter can be proved sound, however such proofs are significantly harder to do on the actual implementation of an analyser. To alleviate this problem we propose to generate Verification Conditions (VCs, formulae valid only if the results of the analyser are correct) and to discharge them using an Automated Theorem Prover (ATP). We generate formulae in Many-Sorted First-Order Logic (MSFOL), a logic that has been successfully used in deductive program verification. MSFOL is expressive enough to describe the results of complex analyses and to formalise the operational semantics of object-oriented languages. Using the same logic for both tasks allows us to prove the soundness of the VC generator using deductive verification tools. To ensure that VCs can be automatically discharged for complex analyses of the heap, we introduce a VC calculus that produces formulae belonging to a decidable fragment of MSFOL. Furthermore, to be able to certify different analyses with the same calculus, we describe a family of analyses with a parametric concretisation function and instrumentation of the semantics. To improve the reliability of ATPs, we also studied the result certification of Satisfiability Modulo Theory solvers, a family of ATPs dedicated to MSFOL. We propose a modular proof-system and a modular proof-verifier programmed and proved correct in Coq, that rely on exchangeable verifiers for each of the underlying theories.

Πολλές εφαρμογές ψηφιακής επεξεργασίας σημάτων (DSP) και πολυμέσων μπορούν να ωφεληθούν από τη χρήση ενός αριθμητικού συστήματος υπολοίπων (RNS). Ανάμεσα στους πιο συχνά χρησιμοποιούμενους διαιρέτες σε τέτοια συστήματα είναι αυτοί της μορφής 2^n - 1 και 2^n + 1, ενώ ανάμεσα στις πιο συχνά χρησιμοποιούμενες λειτουργίες βρίσκονται ο πολλαπλασιασμός και το άθροισμα τετραγώνων. Οι λειτουργίες αυτές προς το παρόν υλοποιούνται με τη χρήση ξεχωριστών μονάδων και συνεχόμενων κύκλων μηχανής. Στην παρούσα εργασία προτείνονται δύο αρχιτεκτονικές για μονάδες οι οποίες μπορούν να εκτελέσουν είτε το X * Y είτε το X^2 + Y^2, ανάλογα με την τιμή ενός σήματος ελέγχου. Εξετάζεται τόσο η modulo 2^n - 1, όσο και η ελαττωμένη κατά ένα modulo 2^n + 1 αριθμητική. / Digital signal processing (DSP) and multimedia applications often profit from the use of a Residue Number System (RNS). Among the most commonly used moduli in such systems are those of 2^n - 1 and 2^n + 1 form and among the most commonly used operations are multiplication and sum-of-squares. These operations are currently performed using distinct design units and consecutive machine cycles. In this paper, we propose two architectures for units that perform either the X * Y or the X^2 + Y^2 operation depending on the value of a control signal. Both modulo 2^n - 1 and diminished-1 2^n + 1 arithmetic is considered.

This thesis focuses on the Binary Integer Modulo-Division Algorithm that is essential for the permutation process in Sunar-Koc ONB Type II Multiplier and also for other general purposes. This thesis explains the new algorithm developed based on the systolic array architecture which gives a systematic approach to the iterative process for the Modulo-Division. The scheduling and projection timing functions are proposed for the processor array allocation and the matlab code has been implemented to verify the efficiency of the algorithm. The thesis also explores the possibility of word based algorithm for design optimisation. / Graduate / 0544 / 0984 / m.shubha8@gmail.com

In recent years, Satisfiability Modulo Theories (SMT) solvers have emerged as powerful tools in many formal methods applications, including verification, automated theorem proving, planning and software synthesis. The expressive power of SMT allows problems from many disciplines to be handled in a single unified approach. While SMT solvers are highly effective at handling certain classes of problems due to highly tuned implementations of efficient ground decision procedures, their ability is often limited when reasoning about universally quantified first-order formulas. Since generally this class of problems is undecidable, most SMT solvers use heuristic techniques for answering unsatisfiable when quantified formulas are present. On the other hand, when the problem is satisfiable, solvers using these techniques will either run indefinitely, or give up after some predetermined amount of effort. In a majority of formal methods applications, it is critical that the SMT solver be able to determine when such a formula is satisfiable, especially when it can return some representation of a model for the formula. This dissertation introduces new techniques for finding models for SMT formulas containing quantified first-order formulas. We will focus our attention on finding finite models, that is, models whose domain elements can be represented as a finite set. We give a procedure that is both finite model complete and refutationally complete for a fragment of first-order logic that occurs commonly in practice.

Automated planning as a satisfiability problem is a method developed in theearly nineties. It has some known disadvantages, such as its inefficient encod-ing of numbers. The field of Satisfiability Modulo Teories tries to connectalready established solvers for e.g. linear constraints into SAT-solvers in orderto make reasoning about numerical values more efficient. This thesis combines planning as satisfiability and SMT to perform efficientreasoning about actions that occupy realistic time in Temporal Action Logic,a formalism developed at Linköping University for reasoning about action andchange.

In wireless communication systems, we may encounter many problems. One of the main issues is noise interference. To overcome the problem, the sender can use the Convolutional coding method to encode the data, and the receiver can utilize the Viterbi algorithm for decoding and correction purposes. Due to the high complexity of the Viterbi algorithm, the VLSI structure of Viterbi decoder will consume large amounts of power, leading the portable devices to short standby time and high operating temperature. In order to solve these problems we have to design a low power decoder. As a matter of fact, the Viterbi decoder can be actually shutdown when no noise interference exists. As a consequence, we use a detection circuit to determine whether the signal is influenced by noise. If the signal is interfered, we choose the Viterbi decoder to perform the decoding process. Otherwise, we utilize a low cost decoder to lessen the power consumed at the receiver end. In addition, dynamic adjustment of SMU module is also developed and implemented in the proposed decoder. SMU module consumes the most power in Viterbi decoder. So, our developed and goal is to reduce the usage of SMU module. If noise distribution is not so dense, we don¡¦t have to use high decoding ability to decode section data. Therefore, the registers in SMU can be decreased. Clock gating technique is adopted in this thesis to shutdown these idle registers to reduce the power consumption of SMU. The proposed decoder has been implemented and synthesized using the Artisan TSMC 0.13£gm standard cell library. Compared with the traditional Viterbi decoder, the proposed decoder can achieve 25% and nearly 60% power saving when the SNR is 1dB and 8dB respectively, with 6% area reduction. According to the above experimental results, we can say that the proposed decoder is able to reduce power consumption.

Due to the continued development of Internet technology, more and more people are willing to take advantage of high-interaction and diverse web applications to deal with commercial, knowledge-sharing, and social activities. However, while web applications deeply affect our society by degrees, hackers start exploiting web application vulnerabilities to attack innocent end user and back-end database, and therefore pose significant threat in information security. According to this situation, this paper proposes a detection mechanism based on Model Checking to detect web application vulnerabilities. We reduce the problem whether the vulnerabilities exist or not to a kind of SMT (Satisfiability Modulo Theories) problem, and analyze all of the traces of tainted data flow in web applications to find possible vulnerabilities by SMT solver. The experimental results show that the method we proposed can identify SQL injection and XSS vulnerabilities effectively, and prove our method is a feasible way to find web application vulnerabilities.