Search

This study investigated the corrosion behaviour of commercial and model Fe- and Ni-based alloys in solar salt at 600°C. The thermal decomposition of nitrate salts led to an increasing concentration of oxidizing agents in the salt melt and thus to a higher corrosion rate. For Fe-based alloys, the oxide scales contained a Na- and Fe-rich outer layer, followed by an inner Cr-rich layer and nitridation as well as Cr-depletion was observed at the scale/metal interface. Furthermore, higher extent of chloride impurities in solar salt, led to a significantly higher corrosion rate for ferritic-martensitic alloys. For Ni-based alloys, the formation of a duplex scale consisting of a NiO outer and Ni-Cr spinel layer showed protective character during isothermal exposure; however even for Ni-based alloys, Cr was detected in the salt melt, which showed evidence for its dissolution in the melt as toxic hexavalent Cr. Diffusion aluminide and electroless Ni-P coatings deposited on cost-efficient ferriticmartensitic alloys led to formation of protective oxide scales and hindered the Cr-dissolution into the salt melt. info:eu-repo/semantics/publishedVersion

In this paper we describe the design and implementation of feqb, a tool that synthesizes sound equality tests for inductive data types in the dependent type theory of the Coq system. Our procedure scales to large inductive data types, as in hundreds of constructors, since the terms and proofs it synthesizes are linear in the size of the inductive type. Moreover it supports some forms of dependently typed arguments and sigma types pairing data with proofs of decidable properties. Finally feqb handles deeply nested containers without requiring any human intervention.

Timing side-channels are arguably one of the main sources of vulnerabilities in cryptographic implementations. One effective mitigation against timing side-channels is to write programs that do not perform secret-dependent branches and memory accesses. This mitigation, known as "cryptographic constant-time", is adopted by several popular cryptographic libraries. This paper focuses on compilation of cryptographic constant-time programs, and more specifically on the following question: is the code generated by a realistic compiler for a constant-time source program itself provably constant-time? Surprisingly, we answer the question positively for a mildly modified version of the CompCert compiler, a formally verified and moderately optimizing compiler for C. Concretely, we modify the CompCert compiler to eliminate sources of potential leakage. Then, we instrument the operational semantics of CompCert intermediate languages so as to be able to capture cryptographic constant-time. Finally, we prove that the modified CompCert compiler preserves constant-time. Our mechanization maximizes reuse of the CompCert correctness proof, through the use of new proof techniques for proving preservation of constant-time. These techniques achieve complementary trade-offs between generality and tractability of proof effort, and are of independent interest.

International audience; Power and electromagnetic based side-channel attacks are serious threats against the security of cryptographic embedded devices. In order to mitigate these attacks, implementations use countermeasures, among which masking is currently the most investigated and deployed choice. Unfortunately, commonly studied forms of masking rely on underlying assumptions that are difficult to satisfy in practice. This is due to physical defaults, such as glitches or transitions, which can recombine the masked data in a way that concretely reduces an implementation's security. We develop and implement an automated approach for verifying security of masked implementations in presence of physical defaults (glitches or transitions). Our approach helps to recover the main strengths of masking: rigorous foundations, composability guarantees, automated verification under more realistic assumptions. Our work follows the approach of (Barthe et al, EUROCRYPT 2015) and thus contributes to demonstrate the benefits of language-based approaches (specifically probabilistic information flow) for masking.

The selection of materials is of utmost importance in gas turbine engines to ensure the security of the passengers, optimize the performances of the aircraft and be cost efficient. In the hottest region of the engines (i.e. combustion chamber and turbine), the components are usually made of nickel-based superalloys. These materials can resist to high mechanical loads at high temperature but are vulnerable to aggressive environments. Therefore, nickel-based superalloys are usually coated to increase their durability in the engine (surface engineering). The chemical composition and the coating architecture are carefully adjusted depending on the temperature regime and the mechanisms of degradation encountered (hot corrosion, oxidation and/or erosion). New synthesis routes and functionalization are currently developed as alternative solutions to industrial processes. As a promising alternative approach, different studies were carried out in the LaSIE laboratory under the European project “PARTICOAT” and confirmed the possibility to elaborate complete thermal barrier systems (diffusion coating + thermal barrier coating) from Al-containing water-based slurries. In this work, the role of Cr as a doping agent was investigated. The addition of Cr decreased the thermodynamic activity of Al upon aluminizing and limited the exothermic reactions usually reported between Al and nickel-based materials. Different architectures of coatings were obtained thanks to the flexibility and the adaptability of the slurry coating process. The gas composition (Ar, air) and the heat treatment conditions were also investigated. Finally, the high temperature resistance of the slurry coatings developed during this work was evaluated under hot corrosion and oxidation conditions.; La sélection des matériaux utilisés dans les moteurs aéronautiques est un enjeu majeur pour assurer la sécurité des passagers, optimiser les performances de l’avion et maîtriser les coûts. Dans les parties les plus chaudes des moteurs (i.e. chambre de combustion et turbine), les pièces sont généralement constituées de superalliages à base nickel en raison de leurs excellentes propriétés mécaniques à haute température. Vulnérables aux phénomènes de corrosion et d’oxydation à haute température, les superalliages doivent la plupart du temps être revêtus afin de prolonger leur durée de vie (ingénierie de surface). La composition chimique et l’architecture des revêtements sont alors adaptées en fonction du régime de température et des phénomènes de dégradation rencontrés (i.e. corrosion à chaud, oxydation et/ou érosion). En vue de répondre aux nouvelles réglementations environnementales, de nouvelles voies de synthèse et de fonctionnalisation sont à l’étude comme alternatives aux procédés industriels actuels. Dans le cadre du projet Européen « PARTICOAT », le LaSIE a démontré la faisabilité d’élaborer des systèmes barrières thermiques complets (couche de diffusion + barrière thermique) en une seule étape à partir de barbotines (« slurries ») à base aqueuse contenant des microparticules d’Al. Dans cette étude, l’ajout de Cr comme dopant a été étudié. L’addition de Cr a permis d’abaisser l’activité de l’Al lors de l’étape d’aluminisation et de limiter les réactions exothermiques entre Al et substrat à base de nickel. L’optimisation des ratios entre Al et Cr a permis d’obtenir différentes microstructures de revêtement. Diverses architectures de dépôts ont également pu être testées grâce à la souplesse d’élaboration des revêtements par barbotines. L’influence de l’atmosphère (Ar, air) et celle des conditions de traitement thermique ont également été étudiées. Enfin, la durabilité des revêtements développés au cours de la thèse a été évaluée au cours d’essais de corrosion à chaud et d’oxydation.

The selection of materials is of utmost importance in gas turbine engines to ensure the security of the passengers, optimize the performances of the aircraft and be cost efficient. In the hottest region of the engines (i.e. combustion chamber and turbine), the components are usually made of nickel-based superalloys. These materials can resist to high mechanical loads at high temperature but are vulnerable to aggressive environments. Therefore, nickel-based superalloys are usually coated to increase their durability in the engine (surface engineering). The chemical composition and the coating architecture are carefully adjusted depending on the temperature regime and the mechanisms of degradation encountered (hot corrosion, oxidation and/or erosion). New synthesis routes and functionalization are currently developed as alternative solutions to industrial processes. As a promising alternative approach, different studies were carried out in the LaSIE laboratory under the European project “PARTICOAT” and confirmed the possibility to elaborate complete thermal barrier systems (diffusion coating + thermal barrier coating) from Al-containing water-based slurries. In this work, the role of Cr as a doping agent was investigated. The addition of Cr decreased the thermodynamic activity of Al upon aluminizing and limited the exothermic reactions usually reported between Al and nickel-based materials. Different architectures of coatings were obtained thanks to the flexibility and the adaptability of the slurry coating process. The gas composition (Ar, air) and the heat treatment conditions were also investigated. Finally, the high temperature resistance of the slurry coatings developed during this work was evaluated under hot corrosion and oxidation conditions.; La sélection des matériaux utilisés dans les moteurs aéronautiques est un enjeu majeur pour assurer la sécurité des passagers, optimiser les performances de l’avion et maîtriser les coûts. Dans les parties les plus chaudes des moteurs (i.e. chambre de combustion et turbine), les pièces sont généralement constituées de superalliages à base nickel en raison de leurs excellentes propriétés mécaniques à haute température. Vulnérables aux phénomènes de corrosion et d’oxydation à haute température, les superalliages doivent la plupart du temps être revêtus afin de prolonger leur durée de vie (ingénierie de surface). La composition chimique et l’architecture des revêtements sont alors adaptées en fonction du régime de température et des phénomènes de dégradation rencontrés (i.e. corrosion à chaud, oxydation et/ou érosion). En vue de répondre aux nouvelles réglementations environnementales, de nouvelles voies de synthèse et de fonctionnalisation sont à l’étude comme alternatives aux procédés industriels actuels. Dans le cadre du projet Européen « PARTICOAT », le LaSIE a démontré la faisabilité d’élaborer des systèmes barrières thermiques complets (couche de diffusion + barrière thermique) en une seule étape à partir de barbotines (« slurries ») à base aqueuse contenant des microparticules d’Al. Dans cette étude, l’ajout de Cr comme dopant a été étudié. L’addition de Cr a permis d’abaisser l’activité de l’Al lors de l’étape d’aluminisation et de limiter les réactions exothermiques entre Al et substrat à base de nickel. L’optimisation des ratios entre Al et Cr a permis d’obtenir différentes microstructures de revêtement. Diverses architectures de dépôts ont également pu être testées grâce à la souplesse d’élaboration des revêtements par barbotines. L’influence de l’atmosphère (Ar, air) et celle des conditions de traitement thermique ont également été étudiées. Enfin, la durabilité des revêtements développés au cours de la thèse a été évaluée au cours d’essais de corrosion à chaud et d’oxydation.

International audience; In this paper, we provide a necessary clarification of the good security properties that can be obtained from parallel implementations of masking schemes. For this purpose, we first argue that (i) the probing model is not straightforward to interpret, since it more naturally captures the intuitions of serial implementations, and (ii) the noisy leakage model is not always convenient, e.g. when combined with formal methods for the verification of cryptographic implementations. Therefore we introduce a new model, the bounded moment model, that formalizes a weaker notion of security order frequently used in the side-channel literature. Interestingly , we prove that probing security for a serial implementation implies bounded moment security for its parallel counterpart. This result therefore enables an accurate understanding of the links between formal security analyses of masking schemes and experimental security evaluations based on the estimation of statistical moments Besides its consolidating nature, our work also brings useful technical contributions. First, we describe and analyze refreshing and multiplication algorithms that are well suited for parallel implementations and improve security against multivariate side-channel attacks. Second, we show that simple refreshing algorithms (with linear complexity) that are not secure in the continuous probing model are secure in the continuous bounded moment model. Eventually, we discuss the independent leakage assumption required for masking to deliver its security promises, and its specificities related to the serial or parallel nature of an implementation.

International audience; We present the construction and implementation of an 8-bit S-box with a differential and linear branch number of 3. We show an application by designing Fly, a simple block cipher based on bitsliced evaluations of the S-box and bit rotations that targets the same platforms as Pride, and which can be seen as a variant of Present with 8-bit S-boxes. The round function of Fly achieves the same performance as the one of Pride on 8-bit microcontrollers (in terms of number of instructions per round and code size) while having 1.5 times more equivalent active S-boxes on average. The S-box also has an efficient implementation with SIMD instructions, a low implementation cost in hardware and it can be masked efficiently thanks to its sparing use of non-linear gates and to the fact that it has a natural expression in terms of a single 4-bit S-box.

International audience; Boolean reflection is a formalization technique that represents decidable predicates with their decision procedures and where truth values become booleans. Reflection occurs in the small scale: since conjectures are stated using programs their symbolic execution provides a valuable form of automation. In this approach the user faces the " syntactic " (bool) representation of the conjecture and is given tactic-level tools to switch to the " semantic " one (Prop) and back. The SSReflect proof language [1] provides the view mechanism to switch from the computational realm of bool to the semantic one of Prop. To minimize the syntactic noise due to view application SSReflect accepts views as annotations of most linguistic constructs. Still a user needs to mention the view name explicitly, even when there is only one view to be applied. We propose a type-class [2] based machinery to attach canonical views to predicates and connectives to relief the Coq user from some of the bookkeeping required by the boolean reflection formalization technique. Let's take a very simple example. Here the is_true constant is used to state the truth of a boolean predicates. Being declared as a coercion is automatically inserted by Coq around any boolean value occurring in a context expecting a Prop. The support lemmas andP and orP are views linking the boolean connec-tives && and || to their meaning in Prop. The reflect predicate simply states that its first argument, in Prop, holds if and only its second argument, in bool, is equal to true. Definition is_true b := b = true. Coercion is_true : bool >-> Sortclass. (* Prop *) Lemma andP b1 b2 : reflect (b1 /\ b2) (b1 && b2). Lemma orP b1 b2 : reflect (b1 \/ b2) (b1 || b2). Lemma example_bool a b : ((a && b) || a)-> a Proof. by move=> /orP[ /andP[ Ha Hb ] | Ha ]; assumption. Qed. Lemma example_prop a b : ((a /\ b) \/ a)-> a Proof. by move=> [ [ Ha Hb ] | Ha ]; assumption. Qed. The example_bool proof 1 applies the two views in order to de-structure the assumption. The second proof needs no such bookkeeping, since the conjecture is already stated in Prop. We propose a declarative way of associating canonical views to connectives and predicates and a generic view name xP to select the view fitting the current 1 A much simples proof would be to enumerate truth values as in " by case a; case b ". For the sake of clarity we picked an oversimple example.

The Coq Development Team

International audience; Cryptographic hash functions provide a basic data authentication mechanism and are used pervasively as building blocks to realize many cryptographic functionalities, including block ciphers, message authentication codes, key exchange protocols, and encryption and digital signature schemes. Since weaknesses in hash functions may imply vulnerabilities in the constructions that build upon them, ensuring their security is essential. Unfortunately, many widely used hash functions, including SHA-1 and MD5, are subject to practical attacks. The search for a secure replacement is one of the most active topics in the field of cryptography. In this paper we report on the first machine-checked and independently-verifiable proofs of collision-resistance and indifferentiability of Merkle-Damg{å}rd, a construction that underlies many existing hash functions. Our proofs are built and verified using an extension of the EasyCrypt framework, which relies on state-of-the-art verification tools such as automated theorem provers, SMT solvers, and interactive proof assistants.

International audience

International audience; Enjoying the power of SAT and SMT solvers in the Coq proof as- sistant without compromising soundness requires more than a yes/no answer from them. SAT and SMT solvers should also return a proof witness that can be checked by an external tool. We propose a fully certified checker for such witnesses written in Coq. It can currently check witnesses from the SAT solvers ZChaff and MiniSat and from the SMT solver VeriT. Experiments highlight the efficiency of this checker. On top of it, new reflexive Coq tactics have been built that can decide a subset of Coq's logic by calling external provers and carefully checking their answers.

The efficiency of concentrated solar power technology is based on the functionality of exterior and interior absorber tube surfaces. While a high solar absorptivity and thermocyclic oxidation resistance are targeted for the exterior surfaces, a high resistance against molten nitrate corrosion is essential for the functionality of the interior surfaces. In this study, a bi-layer coating concept combining a Cr-diffusion coating with a top-coat ensured a high thermocyclic oxidation resistance together with high absorptivity for the exterior surfaces. For the interior surfaces, the molten nitrate corrosion resistance of ferritic-martensitic steels was significantly increased via the application of diffusion aluminide coatings.

We propose a probabilistic Hoare logic aHL based on the union bound, a tool from basic probability theory. While the union bound is simple, it is an extremely common tool for analyzing randomized algorithms. In formal verification terms, the union bound allows flexible and compositional reasoning over possible ways an algorithm may go wrong. It also enables a clean separation between reasoning about probabilities and reasoning about events, which are expressed as standard first-order formulas in our logic. Notably, assertions in our logic are non-probabilistic, even though we can conclude probabilistic facts from the judgments. Our logic can also prove accuracy properties for interactive programs, where the program must produce intermediate outputs as soon as pieces of the input arrive, rather than accessing the entire input at once. This setting also enables adaptivity, where later inputs may depend on earlier intermediate outputs. We show how to prove accuracy for several examples from the differential privacy literature, both interactive and non-interactive.

The efficiency of concentrated solar power technology is based on the functionality of exterior and interior absorber tube surfaces. While a high solar absorptivity and thermocyclic oxidation resistance are targeted for the exterior surfaces, a high resistance against molten nitrate corrosion is essential for the functionality of the interior surfaces. In this study, a bi-layer coating concept combining a Cr-diffusion coating with a top-coat ensured a high thermocyclic oxidation resistance together with high absorptivity for the exterior surfaces. For the interior surfaces, the molten nitrate corrosion resistance of ferritic-martensitic steels was significantly increased via the application of diffusion aluminide coatings.

Since the energy conversion efficiency of CSP systems is directly linked to the operating temperature of the molten salt, the next-generation of CSP plants is targeted to operate at temperatures over 700°C. Due to their higher thermal stability compared to nitrate salts, molten chloride salts are considered as a promising HTF candidate for the next-gen CSP plants. Despite the competitiveness of molten chlorides as HTF, structural materials (i.e. iron and nickel-based alloys) experience severe corrosion in chloride mixtures. Therefore, the second part of this study investigates the corrosion mechanisms of P91 and Inconel 600 in flowing Ar with partial embedding in molten NaCl-KCl and in molten NaCl-KCl-MgCl2 at 700°C. Improvement of scaling behavior of low-Cr steels in molten nitrates allows their application in modern CSP plants thereby increasing the cost-efficiency. Understanding the prevailing corrosion mechanisms in molten chlorides will further develop material selection and corrosion mitigation strategies.

Since the energy conversion efficiency of CSP systems is directly linked to the operating temperature of the molten salt, the next-generation of CSP plants is targeted to operate at temperatures over 700°C. Due to their higher thermal stability compared to nitrate salts, molten chloride salts are considered as a promising HTF candidate for the next-gen CSP plants. Despite the competitiveness of molten chlorides as HTF, structural materials (i.e. iron and nickel-based alloys) experience severe corrosion in chloride mixtures. Therefore, the second part of this study investigates the corrosion mechanisms of P91 and Inconel 600 in flowing Ar with partial embedding in molten NaCl-KCl and in molten NaCl-KCl-MgCl2 at 700°C. Improvement of scaling behavior of low-Cr steels in molten nitrates allows their application in modern CSP plants thereby increasing the cost-efficiency. Understanding the prevailing corrosion mechanisms in molten chlorides will further develop material selection and corrosion mitigation strategies.

We present a high-assurance and high-speed implementation of the SHA-3 hash function. Our implementation is written in the Jasmin programming language, and is formally verified for functional correctness, provable security and timing attack resistance in the EasyCrypt proof assistant. Our implementation is the first to achieve simultaneously the four desirable properties (efficiency, correctness, provable security, and side-channel protection) for a non-trivial cryptographic primitive. Concretely, our mechanized proofs show that: 1) the SHA-3 hash function is indifferentiable from a random oracle, and thus is resistant against collision, first and second preimage attacks; 2) the SHA-3 hash function is correctly implemented by a vectorized x86 implementation. Furthermore, the implementation is provably protected against timing attacks in an idealized model of timing leaks. The proofs include new EasyCrypt libraries of independent interest for programmable random oracles and modular indifferentiability proofs.

This paper introduces notions of resource policy for mobile code to be run on smart devices, to integrate with the proof-carrying code architecture of the Mobile Resource Guarantees (MRG) project. Two forms of policy are used: guaranteed policies which come with proofs and target policies which describe limits of the device. A guaranteed policy is expressed as a function of a methods input sizes, which determines a bound on consumption of some resource. A target policy is defined by a constant bound and input constraints for a method. A recipient of mobile code chooses whether to run methods by comparing between a guaranteed policy and the target policy. Since delivered code may use methods implemented on the target machine, guaranteed policies may also be provided by the platform; they appear symbolically as assumptions in delivered proofs. Guaranteed policies entail proof obligations that must be established from the proof certificate. Before proof, a policy checker ensures that the guaranteed policy refines the target policy; our policy format ensures that this step is tractable and does not require proof. Delivering policies thus mediates between arbitrary target requirements and the desirability to package code and certificate only once.