Dynamically Typed Assembly Language (D-TAL) is not only a lightweight and effective solution to the gap generated by the drop in security produced by the translation of high-level language instructions to low-level language instructions, but it considerably eases up the burden generated by the level of complexity required to implement typed assembly languages statically. Although there are tradeoffs between the static and dynamic approaches, focusing on a dynamic approach leads to simpler, easier to reason about, and more feasible ways to understand deployment of types over monomorphically-typed or untyped intermediate languages. On this occasion, DISM, a simple but powerful and mature untyped assembly language, is extended by the addition of type annotations (on memory and registers) to produce an instance of D-TAL. Strong-DISM, the resulting language, statically, lends itself to simpler analysis about type access and security as the correlation between datatypes and instructions with their respective memory and registers becomes simpler to observe; while dynamically, it disallows operations and further eliminates conditions that from high level languages could be used to violate/circumvent security.

Denna C-uppsats i socialpsykologi syftar till att undersöka hur en grupp gymnasieelever reflekterar kring sina egna och andras erfarenheter av grupptryck. Arbetet ska bidra till att få en förståelse för socialpsykologiska interaktioner som återfinns i resonemanget kring grupptryck. Arbetet grundar sig på intervjuer av fem gymnasielevers upplevelser av grupptryck och använder hermeneutiken i sin metodologi. Empirin analyseras genom tre teorier som behandlar olika perspektiv på grupptryck; beteende, existentiellt och intersubjektivt. Dessa teorier är Social Proof, Sartres Ond Tro samt Meads intersubjektivitet. Vid arbetets slutfas har jag funnit att det existerar tre influenser som gör att man kan dra till sig grupptryck och som har negativa konsekvenser. Dessa tre krafter är, för det första, en önskan om maktlöshet för att fly ångest, för det andra, en osäkerhet som baseras på att andra vet bättre och, slutligen, en överidentifikation med samhällsrollen som utelämnar den lekfulla delen av självet.

De quels critères disposons-nous pour évaluer la validité d’une opinion ?La<p>première partie de la thèse revient sur les tentatives des approches contemporaines<p>de l’argumentation de répondre à cette question. Les approches normatives<p>(pragma-dialectique et logique informelle) évaluent la construction des preuves à<p>l’aune d’un idéal de rationalité, lui-même garanti par un ensemble de règles quant à<p>la construction et la formulation publique des arguments. Les approches descriptives<p>(travaux de Plantin et Doury en particulier) se fondent sur une critique de cette<p>méthode :en prétendant fournir des évaluations objectives des arguments, les<p>théoriciens normatifs s’engagent dans le processus argumentatif et, en définitive,<p>produisent des contre-argumentations et non des évaluations. C’est à l’aune du<p>problème du statut épistémologique de la preuve en histoire que j’ai choisi d’illustrer<p>les limites de l’approche descriptive. En particulier, l’oeuvre du critique littéraire<p>Hayden White se caractérise par une même relation entre (1) un scepticisme sur la<p>possibilité d’établir des critères de rationalité et (2) un parti-pris descriptif :les<p>explications historiques pourraient être décrites comme autant de figures rhétoriques,<p>mais on ne saurait définir un critère permettant d’en évaluer la validité. Comme l’a<p>bien montré Carlo Ginzburg, le scepticisme de White ouvre la porte à toutes les<p>dérives négationnistes.<p>Partant, dans une seconde partie, je propose un modèle d’analyse alternatif. Ce<p>modèle s’appuie sur la définition de la rhétorique comme une dunamis par Aristote :<p>une capacité perfectible à porter un regard technique sur les preuves. Il s’agit,<p>concrètement, de prendre en compte trois points de vues sur la preuve :(1) le point<p>de vue de l’orateur qui invente ses preuves face à un problème concret ;(2) le point<p>de vue de l’artisan qui façonne la matière persuasive; (3) le point de vue de<p>l’auditoire qui reçoit les preuves. L’exercice de ces trois points de vues permet à<p>l’analyste de juger les choix rhétoriques d’un orateur à l’aune de sa propre<p>conscience, perfectible par l’exercice, des alternatives possibles et de leur pertinence<p>en fonction des auditoires concernés. Le critère de rationalité n’est alors pas idéaliste<p>ou transcendant, il est humaniste (Chaïm Perelman, Emmanuelle Danblon) :il est de<p>l’ordre de l’expérience acquise.<p>Dans une troisième partie, j’applique mon modèle à trois ouvrages d’histoire :<p>(1) Les traites négrières d’Olivier Pétré-Grenouilleau ;(2) La vie fragile d’Arlette<p>Farge ;(3) The Ascent of Money de Niall Ferguson. Dans chaque cas, j’évalue les<p>choix rhétoriques des historiens (quant aux usages des preuves extra-techniques et<p>à la construction des trois preuves techniques) au regard des problèmes<p>épistémologiques qu’ils affrontent* et des auditoires potentiels auxquels ils<p>s’adressent. Dans chaque cas, je consacre une partie de l’analyse aux réactions<p>suscitées par leurs ouvrages. Ce faisant, je peux mesurer le caractère anti-rhétorique<p>des pratiques actuelles de la critique :le repérage d’une figure de rhétorique<p>(analogie ou métaphore), d’une forte personnalité ou d’un appel aux émotions<p>suffisent à disqualifier un argument aux yeux des critiques. En d’autres termes, notre<p>tradition critique est pétrie d’illusions normatives et, en premier lieu, l’illusion selon<p>laquelle une preuve pourrait être administrée sans technique. Je conclus en montrant<p>que ces illusions, entretenues par notre tradition philosophique, nous ont fait perdre<p>beaucoup de temps dans le développement d’une formation à l’argumentation qui<p>soit de nature à exercer la dunamis critique des étudiants.<p><p>*<p>(1) établir la vérité historique sur un sujet à fort potentiel polémique ;(2) exprimer les intuitions de la<p>phase de découverte ;(3) formuler et justifier une prédiction. / Doctorat en Langues et lettres / info:eu-repo/semantics/nonPublished

Thesis title: Burden of proof in civil procedure This paper deals with burden of proof. The aim of this thesis is to provide a broader framework for this burden, since it is absolutely crucial in order to form a proper understanding of this topic. The first chapter mentions principles that are common to all legal procedures and those that are applicable only within civil procedure. These general procedural principles need to be interpreted in accordance with the European Convention on Human Rights, which is binding upon Czech law. They also serve as a tool for a deeper integration of European law. The principles that are only applicable within civil procedure are usually presented in pairs consisting of principles of opposite meaning and are never really used in their pure form. The second chapter deals with basic rules of Evidence. It mentions the definition of Evidence, it makes a clear distinction between logical methods of proving and procedural ones, followed by definition of the purpose of Evidence. It also mentions topics that do not need to be proven, since there is some type of presumption governing these issues or they are somehow known to the court. This chapter emphasizes tools that simplify the process of proving. It also defines basic terms of Evidence. It does not try to be a complex...

L'analyse statique des programmes permet d'étudier les comportements possibles des programmes sans les exécuter. Les analyseurs statiques sont employés par exemple pour garantir que l'exécution d'un programme ne peut pas produire d'erreurs. Ces outils d'analyse étant eux-mêmes des programmes, ils peuvent être incorrects. Pour accroître la confiance que l'on peut accorder aux résultats d'une telle analyse, nous étudions dans cette thèse comment on peut formellement établir la correction de l'implantation d'un tel analyseur statique. En particulier, nous construisons au moyen de l'assistant à la preuve Coq des interpréteurs abstraits et prouvons qu'ils sont corrects ; c'est-à-dire nous établissons formellement que le résultat de l'analyse d'un programme caractérise bien toutes les exécutions possibles de ce programme. Ces interpréteurs abstraits s'intègrent, dans la mesure du possible, au compilateur vérifié CompCert, ce qui permet de garantir que les propriétés de sûreté prouvées sur le code source d'un programme sont aussi valides pour la version compilée de ce programme. Nous nous concentrons sur l'analyse de programmes écrits dans des langages de bas niveau. C'est-à-dire des langages qui ne fournissent que peu d'abstractions (variables, fonctions, objets, types…) ou des abstractions que le programmeur a loisir de briser. Cela complexifie la tâche d'un analyseur qui ne peut pas s'appuyer sur ces abstractions pour être précis. Nous présentons notamment comment reconstruire automatiquement le graphe de flot de contrôle de programmes binaires auto-modifiants et comment prouver automatiquement qu'un programme écrit en C (où l'arithmétique de pointeurs est omniprésente) ne peut pas produire d'erreurs à l'exécution. / Static analysis of programs enables to study the possible behaviours of programs without running them. Static analysers may be used to guarantee that the execution of a program cannot result in a run-time error. Such analysis tools are themselves programs: they may have bugs. So as to increase the confidence in the results of an analysis, we study in this thesis how the implementation of static analysers can be formally proved correct. In particular, we build abstract interpreters within the Coq proof assistant and prove them correct. Namely, we formally establish that analysis results characterize all possible executions of the analysed program. Such abstract interpreters are integrated to the formally verified CompCert compiler, when relevant ; this enables to guarantee that safety properties that are proved on source code also hold for the corresponding compiled code. We focus on the analysis of programs written in low-level languages. Namely, languages which feature little or no abstractions (variables, functions, objects, types…) or abstractions that the programmer is allowed to break. This hampers the task of a static analyser which thus cannot rely on these abstractions to yield precise results. We discuss in particular how to automatically recover the control-flow graph of binary self-modifying programs, and how to automatically prove that a program written in C (in which pointer arithmetic is pervasive) cannot produce a run-time error.

A travers le système de l’intime conviction les Constituants consacrent un système de liberté de la preuve àl’opposé du système de preuve légale en vigueur sous l’Ancien Régime. L’intime conviction repose sur lacertitude morale des jurés et fait appel à leur conscience citoyenne et religieuse. A la sanction légale lesConstituants ont substitué une sanction morale. Face à l’émergence des preuves scientifiques au XIXème siècle, lesystème de l’intime conviction, remis en cause, continue néanmoins d’incarner le système de preuve le plus à apteà découvrir la vérité et à protéger la liberté individuelle. Au cours de la période contemporaine, la perted’indépendance des jurés vis-à-vis des magistrats professionnels d’une part et l’introduction d’une motivation desarrêts de la cour d’assises d’autre part questionnent à nouveau le système de l’intime conviction. La pérennité dusystème de l’intime conviction suppose un renforcement du poids décisionnel des jurés dans le jugement de lacour d’assises et une revalorisation de leur rôle au cours du procès pénal. L’exigence de motivation de laculpabilité des arrêts de la cour d’assises instaurée par la loi du 10 août 2011 sur la participation des citoyens aufonctionnement de la justice et le jugement des mineurs se révèle minimale. Au regard des exigences du droit auprocès équitable, il convient d’une part de renforcer la motivation de la culpabilité et d’étendre d’autre part lamotivation des arrêts de la cour d’assises à la peine prononcée. L’intégration des exigences du droit au procèséquitable en matière de motivation dans notre procédure pénale, constitue une chance pour le système de l’intimeconviction, ainsi appelé à se renouveler. / Through the system of the firm conviction, the constituents consecrate a system of freedom of the proof opposite to the system of legal proof applicable under the former regime. The firm conviction is based on the moral certitude of the jurors and involves their civic and religious consciousness. The constituents have substituted the legal sanction by a moral sanction. With the emergence of scientific proofs during the XIXth century, the system of firm conviction, although challenged, however continues to embody the proof system that is the most suitable to discover the truth and protect individual freedom. Over the contemporary period, the loss of independence of jurors towards professional judges on one end and the introduction of the requirement of reasoning for the judgement of assize courts on the other end again question the system of the firm conviction. The sustainability of the system of the firm conviction implies a strenthening to the decisional power of the jurors in the judgement of the assize court and a revalorisation of the role of the jurors during criminal trials. The requirement of the reasoning leading to guilt in the judgement of the assize court established by the law of the 10th August 2011 on the partcipation of the citizens to the functioning of Justice and judgement of minors proves to be insufficient. Regarding the legal requirements for a fair trial, it is necessary to reinforce on one end the reasoning leading to guilt and to extend on the other end the requirement of reasoning to the sentence pronounced by the assize court. The integration of the legal requirements for a fair trial regarding the reasoning in our criminal proceedings represents a chance for the system of the firm conviction which is thus called to renew itself.

Un hyperviseur est un logiciel qui virtualise les ressources d'une machine physique pour permettre à plusieurs systèmes d'exploitation invités de s'exécuter simultanément dessus. L'hyperviseur étant le gestionnaire des ressources, un bug peut être critique pour les systèmes invités. Dans cette thèse nous nous intéressons aux propriétés d'isolation de la mémoire d'un hyperviseur de type 1, qui virtualise la mémoire en utilisant des Shadow Page Tables. Plus précisément, nous présentons un modèle concret et un modèle abstrait de l'hyperviseur, et nous prouvons formellement que les systèmes d'exploitation invités ne peuvent pas altérer ou accéder aux données privées des autres s'ils n'en ont pas la permission. Nous utilisons le langage et l'assistant de preuve développés par Prove & Run pour ce faire. Le modèle concret comporte beaucoup d'optimisations, qui rendent les structures de données et les algorithmes complexes, il est donc difficile de raisonner dessus. C'est pourquoi nous construisons un modèle abstrait dans lequel il est plus facile de raisonner. Nous prouvons les propriétés sur le modèle abstrait, et nous prouvons formellement sa correspondance avec le modèle concret, de telle manière que les preuves sur le modèle abstrait s'appliquent au modèle concret. La preuve correspondance n'est valable que pour des états concrets qui respectent certaines propriétés, nous prouvons que ces propriétés sont des invariants du système concret. La preuve s'articule donc en trois phases : la preuve d'invariants au niveau concret, la preuve de correspondance entre les modèles abstraits et concret, et la preuve des propriétés de sécurité au niveau abstrait. / A hypervisor is a software which virtualizes hardware resources, allowing several guest operating systems to run simultaneously on the same machine. Since the hypervisor manages the access to resources, a bug can be critical for the guest Oses. In this thesis, we focus on memory isolation properties of a type 1 hypervisor, which virtualizes memory using Shadow Page Tables. More precisely, we present a low-level and a high-level model of the hypervisor, and we formally prove that guest OSes cannot access or tamper with private data of other guests, unless they have the authorization to do so. We use the language and the proof assistant developed by Prove & Run. There are many optimizations in the low-level model, which makes the data structures and algorithms complexes. It is therefore difficult to reason on such a model. To circumvent this issue, we design an abstract model in which it is easier to reason. We prove properties on the abstract model, and we prove its correspondence with the low-level model, in such a way that properties proved on the abstract model also hold for the low-level model. The correspondence proof is valid only for low-level states which respect some properties. We prove that these properties are invariants of the low-level system. The proof can be divided into three parts : the proof of invariants preservation on the low-level, the proof of correspondence between abstract and low-level models, and proof of the security properties on the abstract level.

The concept of a recursive function has been extensively studied using traditional tools of computability theory. However, with the development of category-theoretic methods it has become possible to study recursion in a more general (abstract) sense. The particular model this thesis is structured around is known as a Turing category. The structure within a Turing category models the notion of partiality as well as recursive computation, and equips us with the tools of category theory to study these concepts. The goal of this work is to build a formal language description of this computation model. Specifically, to use the Coq proof assistant to formulate informal definitions, propositions and proofs pertaining to Turing categories in the underlying formal language of Coq, the Calculus of Co-inductive Constructions (CIC). Furthermore, we have instantiated the more general Turing category formalism with a CIC description of the category which models the language of partial recursive functions exactly.

Même si elle n’est pas une preuve per se, il est admis de longue date que la présomption peut, provisoirement, faire office de preuve lorsqu’une preuve directe d’un fait est indisponible ou difficile à produire. En l’absence d’un droit de la preuve codifié de l’Union européenne, il n’est pas aisé d’affirmer que les critères de classification des présomptions en droit interne (l’admissibilité de la preuve et l’auteur de la présomption) sont transposables au droit de l’Union. Cela ne signifie pas que la présomption est irrévocablement bannie du vocabulaire juridique de celle-ci ; l’examen de la jurisprudence de la Cour de justice et du droit en vigueur permet d’identifier un certain nombre de circonstances dans lesquelles le législateur et le juge sont amenés à former des présomptions. La pratique en droit de l’Union confirme ainsi un aspect fondamental de la théorie générale de la présomption relatif à la genèse de celle-ci : elle apparaît là où il y a un doute qu’il convient d’éliminer, au moins jusqu’à la production d’une preuve contraire. La nécessité qu’un tel doute soit écarté peut être identifiée a priori (ce qui doit être présumé) ou a posteriori (ce qu’il est permis de présumer), à l’issue des recherches des preuves de certains faits. En ce sens, le droit de l’Union européenne connaît des présomptions qui font office de preuves aprioriques ou prima facie telles que les présomptions tirées du droit international des traités et des organisations internationales, la légalité, la validité, la conformité et l’équivalence des législations, au sens du principe de reconnaissance mutuelle. En revanche, l’on trouve des faits qui peuvent être présumés dans le droit de la concurrence et les relations extérieures de l’Union, dans l’examen des entraves aux libertés de circulation ainsi que dans l’interprétation des traités. Il peut ainsi être soutenu que le droit de l’Union européenne dispose, matériellement, d’un droit des présomptions qui contient ses propres critères liés à la classification et aux effets probatoires de ces dernières. / It is traditionally held that even though it cannot be qualified as evidence per se, presumption can provisionally produce the effect of evidence, when direct evidence is not available, or even possible, of a fact for which such evidence is required. Considering that the EU does not have a codified law on evidence, the criteria known in national law by virtue of which presumptions are either refutable or irrefutable cannot, prima facie, apply in EU law. This does not mean that the notion of presumption has no place in EU legal vocabulary. The analysis of the case law of the EU Courts, as well as of EU secondary law, allows the discerning of the circumstance in which the legislator, or the judge, use presumptions as techniques that provide good, although temporary, solutions to situations characterized by doubt. The practice in EU law thus confirms a crucial point that has been raised in legal theory on evidence: presumption appears where there is a need to eliminate a doubt, through accepting something to be true until the contrary is established. The need that a doubt be removed can arise a priori (what should be presumed) or a posteriori (what can be presumed), when a search for evidence fails to meet a legal standard. There are, indeed, certain facts that should prima facie be held as true in EU law, such as those given by the presumptions taken over from International law of treaties and of International Organizations, the presumptions of legality and validity, of compliance or compatibility and of equivalence within the meaning of the principle of mutual recognition. The facts that can be presumed in EU law are usually facts for which evidence is required in Competition law, the EU external relations, the restrictions on the freedoms of movement and the interpretation of the Treaties. It can thus be held that there is, in the EU, a law on presumptions, which contains its own criteria related to the division of presumptions, as well as to their evidentiary effects.

L’expertise judiciaire pénale consiste à faire intervenir un sachant, spécialiste de son domaine, dans un procès pénal, afin qu’il l’éclaire par sa science. Par la maitrise de son art, l’expert détient une place indispensable au sein de ce procès. Son rôle dans la manifestation de la vérité est essentiel et ne cesse de s’accroitre, notamment du fait des avancées scientifiques. Cette force probante importante influence énormément l’intime conviction des juges. Cela peut se révéler dangereux dans le cadre d’analyses faillibles ou subjectives. Face à ce risque, il est nécessaire d’encadrer strictement chaque étape de la mesure expertale. Ce besoin trouve également son origine dans la confrontation qui peut se produire entre l’expertise et les droits fondamentaux. À l’image de la procédure pénale, cette mesure se heurte à une opposition entre la nécessité de rechercher la vérité afin de protéger l’ordre public et les libertés individuelles atteintes par l’activité de l’expert. L’enjeu de l’encadrement de l’expertise pénale repose donc sur la recherche d’un équilibre entre ces deux objectifs de protection, parfois antagonistes. Cet équilibre se manifeste aussi entre le besoin d’efficacité de la mesure et le respect des règles du procès équitable dans lequel le contradictoire possède une place considérable. Par ailleurs, l’expertise fait face à des obstacles factuels qui peuvent rendre sa mise en œuvre laborieuse. L’encadrement de l’expertise pénale se doit d’en tenir compte. Ainsi, du recrutement de l’expert, jusqu’aux effets du rapport, en passant par la mise en œuvre de la mission, l’encadrement de l’expertise pénale est confronté à des difficultés et répond à un besoin impérieux. Cet encadrement se doit d’être évolutif pour se trouver en conformité avec la société dans laquelle il intervient. Bien que satisfaisant, il reste perfectible. Le système actuel pourrait faire l’objet d’une homogénéisation, dans un but de simplification des procédures. L’encadrement de l’expertise pénale doit être particulièrement simple pour être efficace, car il s’adresse en grande partie aux experts qui, par définition, ne sont pas des spécialistes du droit. / The criminal expertise involves calling upon a specialist, knowledgeable in his/her field to shed light in criminal trial. Because of his/her level of competence, this expert witness is a key element in a criminal trial. His/her role in revealing the truth is essential and even more so when considering scientific progress. This major probative force greatly influences the judges’ personal convictions which can prove risky in the case of fallible and subjective analyses. Accordingly, it is necessary to tightly frame each step of the expert’s testimony. This need also stems from the possible conflict between the expertise and fundamental rights. Just like criminal proceedings, the criminal expertise collides with the contradiction between safeguarding public order by seeking the truth and preventing the expert’s testimony to infringe on individual rights. Therefore, the challenge in framing the criminal expertise lies in finding a balance between these two sometimes conflicting, safeguarding purposes. A need for balance is also evident when considering both the effectiveness of the criminal expertise and the respect of the rules for a fair trial where the principe of audi alteram partem is greatly important. Moreover, the criminal expertise faces factual obstacles which may hinder its implementation. This must be taken into account while establishing the criminal expertise framework. Thus, from the selection of the expert to the impact of the report, through the implementation of the task, the criminal expertise framework has to cope with difficulties and has to answer to a compelling need. This framework must be adjustable and conform to the society to which it applies. Although satisfying, it still could be improved. The current system might be subject to standardization, leading to a simplification of procedures. The criminal expertise framework must be specifically simple to be efficient because it addresses, for the most part, experts who, by definition, are no law experts.