Most modern software attacks are rooted in memory corruption vulnerabilities. They redirect security-sensitive data values (e.g., return address, function pointer, and heap metadata) to an unintended value. Current state-of-the-art policies, such as Data-Flow Integrity (DFI) and Control-Flow Integrity (CFI), are effective but often struggle to balance precision, generality, and runtime overhead. In this thesis, we propose Data-Value Integrity (DVI), a new defense policy that enforces the integrity of "data value" for security-sensitive control and non-control data. DVI breaks an essential step of memory corruption based attacks by asserting the compromised security-sensitive data value. To show the efficacy of DVI, we present HyperSpace, a prototype that enforces DVI to provide four representative security mechanisms. These include Code Pointer Separation (DVI-CPS) and Code Pointer Integrity (DVI-CPI) based on HyperSpace. We evaluate HyperSpace with SPEC CPU2006 and real-world servers. We also test HyperSpace against memory corruption based attacks, including three real-world exploits and six attacks that bypass existing defenses. Our evaluation shows that HyperSpace successfully detects all attacks and introduces low runtime performance and memory overhead: 1.02% and 6.35% performance overhead for DVI-CPS and DVI-CPI, respectively, and overall approximately 15% memory overhead. / Master of Science / Many modern attacks originate from memory corruption vulnerabilities. These attacks, such as buffer overflow, allow an adversary to compromise a system by executing arbitrary code or escalating their access privilege for malicious actions. Unfortunately, this is due to today's common programming languages such as C/C++ being especially prone to memory corruption. These languages build the foundation of our software stack thus, many applications such as web browsers and database servers that are written using these vulnerable programming languages inherit these shortcomings. There have been numerous security mechanisms that are widely adopted to address this issue but they all fall short in providing complete memory security. Since then, security researchers have proposed various solutions to mitigate these ever-growing shortcomings of memory safety techniques. Nonetheless, these defense techniques are either too narrow-scoped, incur high runtime overhead, or require significant additional hardware resources. This results in them being unscalable for bigger applications or requiring it to be used in combination with other techniques to provide a stronger security guarantee. This thesis presents Data Value Integrity (DVI), a new defense policy that enforces the integrity of "data value" for sensitive C/C++ data which includes, function pointers, virtual function table pointers, and inline heap metadata. DVI can offer wide-scoped security while being able to scale, making it a versatile and elegant solution to address various memory corruption vulnerabilities. This thesis also introduces HyperSpace, a prototype that enforces DVI. The evaluation shows that HyperSpace performs better than state-of-the-art defense mechanisms while having less performance and memory overhead and also providing stronger and more general security guarantees.

It is well known that for small Reynolds numbers, flow around a cylinder is laminar and stable. For larger Reynolds numbers, although the flow regime remains laminar, the formation of complex periodic structures appear downstream. The cyclic nature of this periodic flow is well characterized by the vortex shedding frequency and Strouhal number. However, complexities of these periodic structures downstream continue to be a topic of research. Periodic laminar 2D incompressible viscous flow around a cylinder is simulated using OpenFoam, an open source computational fluid dynamics program. To better understand these complex structures downstream, a customized computer graphical tool, VerFlow-V.01, was created to analyze and study OpenFoam simulation results. This study includes an investigation of calculating the details of drag and lift coefficients for the cylinder using mathematical models that integrate properties in subdomains, an approach not previously explored to the knowledge of the author. Numerical integration is accomplished using a finite difference approach for solving surface and contour integrals in subdomains of interest. Special attention is given to pressure and to the second invariant of the velocity gradient, as they have a clear mathematical relationship, which is consistent with results previously published. A customized visual data analysis tool, called VerFlow-V.01, allowed investigators to compare simulation data variables in a variety of useful ways, revealing details not previously understood. Main subroutines and a user's manual are included as appendices to encourage reproducibility and future development of the numerical, analytical and graphical models developed here. Together these models resulted in a new understanding of periodic laminar flow around a cylinder. A unique approach was developed to qualitatively understand the origins of drag and lift coefficients associated with properties mapped as images in subdomains of interest downstream. These results explain the development of convergent, eddy, and stream zones embedded in flow fields downstream. / Master of Science

SMT-based verification analyzes reachability for transition systems represented by SMT formulae. Depending on the theories and the kinds of systems considered, various approaches have been proposed. Together, they form the Verification Modulo Theory (VMT) framework. This thesis delves into SMT-based verification of parameterized systems, emphasizing the challenges and novel solutions in verifying systems with an unbounded number of components. In this thesis, we first introduce a general framework to model such systems. Then, we introduce two novel algorithms that leverage the strengths of SMT for the verification of parameterized systems, focusing on the automation and reduction of computational complexity inherent in such tasks. These algorithms are designed to improve upon existing verification methods by offering enhanced scalability and automation, making them particularly suited for the analysis of distributed systems, network protocols, and concurrent programming models where traditional approaches may fail. Moreover, we introduce an algorithm for compositional verification that advances the capability to modularly verify complex systems by decomposing the verification task into smaller, more manageable sub-tasks. Additionally, we discuss the potential and ongoing application of these algorithms in an industrial project focusing on the design of interlocking logic. This particular application demonstrates the practical utility of our algorithms in a real-world setting, highlighting their effectiveness in improving the safety and reliability of critical infras- tructure. The theoretical advancements proposed in this thesis are complemented by a rig- orous experimental evaluation, demonstrating the applicability and effectiveness of our methods across a range of verification scenarios. Our work is implemented within an ex- tended framework of the MathSAT SMT solver, facilitating its integration into existing verification workflows. Overall, this research contributes to the theoretical underpinnings of Verification Modulo Theories (VMT) and offers tools and methodologies for the verification community, enhancing the capability to verify complex parameterized systems with greater efficiency and reliability.

吀e so-called "trumpet" initial data has recently received mu挀 a琀ention as a potential candidate for the natural black hole initial data to be used in 3+1 numerical relativity simulations with 1+log foliation. In this work we first derive a variant of the maximal trumpet initial data that is made to move on the numerical grid by the means of a Lorentz boost and write a numerical code that constructs this boosted trumpet initial data. We also write a numerical code for calculating the Krets挀mann scalar from the 3+1 variables, to be used in analysing the data from our simulations. With the help of those two codes, we study the behaviour of the boosted trumpet initial data when evolved with the BSSN formulation of the Einstein equations, using 1+log slicing and the Γ-driver shi昀 condition.

Un problème fondamental à résoudre en Automatique réside dans la commande des systèmes incertains qui présentent des contraintes sur les variables de l’entrée, de l’état ou la sortie. Ce problème peut être théoriquement résolu au moyen d’une commande optimale. Cependant la commande optimale par principe n’est pas une commande par retour d’état ou retour de sortie et offre seulement une trajectoire optimale le plus souvent par le biais d’une solution numérique.Par conséquent, dans la pratique, le problème peut être approché par de nombreuses méthodes, tels que”commande over-ride” et ”anti-windup”. Une autre solution, devenu populaire au cours des dernières décennies est la commande prédictive. Selon cette méthode, un problème de la commande optimale est résolu à chaque instant d’échantillonnage, et le composant du vecteur de commande destiné à l’échelon curant est appliquée. En dépit de la montée en puissance des architecture de calcul temps-réel, la commande prédictive est à l’heure actuelle principalement approprié lorsque l’ordre est faible, bien connu, et souvent pour des systèmes linéaires. La version robuste de la commande prédictive est conservatrice et compliquée à mettre en œuvre, tandis que la version explicite de la commande prédictive donnant une solution affine par morceaux implique une compartimentation de l’état-espace en cellules polyédrales, très compliquée.Dans cette thèse, une solution élégante et peu coûteuse en temps de calcul est présentée pour des systèmes linéaire, variant dans le temps ou incertains. Les développements se concentre sur les dynamiques en temps discret avec contraintes polyédriques sur l’entrée et l’état (ou la sortie) des vecteurs, dont les perturbations sont bornées. Cette solution est basée sur l’interpolation entre un correcteur pour la région extérieure qui respecte les contraintes sur l’entrée et de l’état, et un autre pour la région intérieure, ce dernier plus agressif, conçue par n’importe quelle méthode classique, ayant un ensemble robuste positivement invariant associé à l’intérieur des contraintes. Une simple fonction de Lyapunov est utilisée afin d’apporter la preuve de la stabilité en boucle fermée. / A fundamental problem in automatic control is the control of uncertain plants in the presence of input and state or output constraints. An elegant and theoretically most satisfying framework is represented by optimal control policies which, however, rarely gives an analytical feedback solution, and oftentimes builds on numerical solutions (approximations).Therefore, in practice, the problem has seen many ad-hoc solutions, such as override control, anti-windup, as well as modern techniques developed during the last decades usually based on state space models. One of the popular example is Model Predictive Control (MPC) where an optimal control problem is solved at each sampling instant, and the element of the control vector meant for the nearest sampling interval is applied. In spite of the increased computational power of control computers, MPC is at present mainly suitable for low-order, nominally linear systems. The robust version of MPC is conservative and computationally complicated, while the explicit version of MPC that gives an affine state feedback solution involves a very complicated division of the state space into polyhedral cells.In this thesis a novel and computationally cheap solution is presented for linear, time-varying or uncertain, discrete-time systems with polytopic bounded control and state (or output) vectors, with bounded disturbances. The approach is based on the interpolation between a stabilizing, outer controller that respects the control and state constraints, and an inner, more aggressive controller, designed by any method that has a robustly positively invariant set within the constraints. A simple Lyapunov function is used for the proof of closed loop stability.In contrast to MPC, the new interpolation based controller is not necessarily employing an optimization criterion inspired by performance. In its explicit form, the cell partitioning is simpler that the MPC counterpart. For the implicit version, the on-line computational demand can be restricted to the solution of one linear program or quadratic program. Several simulation examples are given, including uncertain linear systems with output feedback and disturbances. Some examples are compared with MPC. The control of a laboratory ball-and-plate system is also demonstrated. It is believed that the new controller might see wide-spread use in industry, including the automotive industry, also for the control of fast, high-order systems with constraints.

Dans une première partie, on se donne un groupe réductif connexe complexe G, et on classifie les modules simples dont le cône des vecteurs primitifs admet une déformation G-invariante non triviale. On relie cette classification à celle des algèbres de Jordan simples, et aussi à celle (due à Akhiezer) des variétés projectives lisses dont les orbites sous l'action d'un groupe algébrique affine connexe sont un diviseur et son complémentaire. Notre principal outil est le schéma de Hilbert invariant d'Alexeev et Brion; on en détermine les premiers exemples. On détermine aussi les déformations infinitésimales (non nécessairement G-invariantes) des cônes des vecteurs primitifs; elles sont triviales pour presque tous les modules simples. Dans une seconde partie, on construit le ``schéma Quot invariant'' et on en détermine une classe d'exemples dans le cas où l'espace ambiant est un cône des vecteurs primitifs.

La théorie d'invariants de type fini des 3-variétés et leurs entrelacs de Goussarov-Habiro repose sur le calcul de claspers, un ensemble d'outils de calcul topologique. Dans cette thèse, on calcule explicitement les invariants en bas degré pour certaines classes d'objets, par une méthode dite graphique. Nous étudions ainsi les cylindres d'homologie sur une surface à 0 ou 1 composante de bord et les string-links framés des boules d'homologie. Leurs invariants de degré 1 sont caractérisés en termes d'invariants classiques, et une correspondance est établie entre les deux cas. On regarde aussi les invariants de Vassiliev des string-links, du point de vue des claspers. Le calcul des invariants de degré 2 implique la construction d'un certain invariant des string-links à 2 cordes. Le lien entre invariants de Vassiliev et de Goussarov-Habiro est étudié pour les string-links.

Dans le cas des systèmes temps-réels, une difficulté majeure pour le développement d’une approche compositionnelle consiste au modèle synchrone du temps où les horloges des différents composants avancent simultanément.Cet aspect est, pourtant, difficile à considérer dans un cadre compositionnel.Nous proposons une méthode basée sur l’approche déductive et consistant à calculer d’une manière purement compositionnelle une sur-approximation de l’ensemble des états atteignables du système à travers un invariant.Ce dernier se compose d’invariants locaux propres aux composants, un invariantd’interaction caractérisant les interactions entre les composants. En plus, afin de considérer le modèle synchrone du temps, nous introduisons des horloges auxiliaires appelées « Horloges d’Histoire ». Elles permettent de générer des invariants supplémentaires permettant de détecter des relations induites par les synchronisations temporelles des différents composants. Appliqué à plusieurs exemples de systèmes, l’invariant s’est avéré souvent suffisamment fort avec une réduction importante de la complexité de vérification.Toutefois, puisque la méthode est basée sur une sur-approximation, des faux contre-exemples peuvent être générés. Nous avons complété la méthode avec un module destiné pour leur analyse.Au delà de son passage à l’échelle, la méthode est étendue pour la vérification uniforme des systèmes paramétrés, où certains composants sont identiques. La validité de la propriété peut être affirmée indépendamment de leur nombre.Cette méthode compositionnelle est implémentée dans l’outil RTD-Finder conçu pour la vérification des systèmes modélisés au langage BIP (Behavior-Interaction-Priority).Les résultats d’expérimentation montrent la réduction de la complexité de vérification en comparaison avec l’approche monolithique, surtout quand l’invariant global est en mesure de détecter la propriété d’intérêt. / The compositional Verification aims at breaking down the complexity of the verification task by relying on the separate analysis of the sub-components and inferring global properties of the system from their local properties.In the framework of real-time systems, one main obstacle for developing fully compositional methods is the synchronous model of time.We propose a verification method based on the deductive approach where the setof reachable states of the system is over-approximated by an invariant computedin a fully compositional manner. It comprises local component invariants andan interaction invariant characterizing the interactions between the components.In addition, we introduce auxiliary clocks, called history clocks which allow toautomatically generate new invariants capturing the constraints induced by thetime-synchronizations between the different components. We completed this com-positional invariant generation approach with a counterexample-based invariantenforcement module analyzing iteratively the generated counterexamples.Besides its scalability, the method can be extended to the uniform verification of parameterized timed systems.Our compositional verification method was implemented in the RTD-Finder tool.The experimental results show that the verification time for large systems is drastically reduced in comparison with exploration techniques, especially when the global invariant catches the safety property of interest.

La géométrie de Cauchy-Riemann, CR en abrégé, est la géométrie naturelle des hypersurfaces réelles pseudoconvexes de $C^{n+1}$, lorsque $ngeq 1$. Nous considérons le cas générique où les variétés CR considérées sont de contact. La géométrie CR présente de nombreuses similarités avec la géométrie conforme ; les invariants mis au jour et les techniques éprouvées en géométrie conforme peuvent donc être adaptées dans ce contexte. Nous nous intéressons dans cette thèse à deux invariants de ce type. Dans une première partie, en utilisant la géométrie asymptotiquement hyperbolique complexe, nous introduisons un opérateur différentiel CR covariant agissant sur les applications allant d'une variété CR vers une variété riemannienne, égal pour les fonctions à l'opérateur de Paneitz CR. Dans une seconde partie, nous proposons un invariant de Yamabe pour les variétés de contact admettant une structure CR, et nous étudions son comportement sous somme connexe. / Cauchy-Riemann geometry, CR for short, is the natural geometry of real pseudoconvex hypersurfaces of $C^{n+1}$ for $ngeq 1$. We consider the generic case when CR manifolds are contact manifolds. CR geometry presents strong analogies with conformal geometry; hence, known invariants and techniques of conformal geometry can be transported to that context. We focus in this thesis on two such invariants. In a first part, using asymptotically complex hyperbolic geometry, we introduce a CR covariant differential operator on maps from a CR manifold to a Riemannian manifold, which coincides on functions with the CR Paneitz operator. In a second part, we propose a Yamabe invariant for contact manifolds which admit a CR structure, and we study its behaviour under connected sum.

abstract: In 1984, Sinnott used $p$-adic measures on $\mathbb{Z}_p$ to give a new proof of the Ferrero-Washington Theorem for abelian number fields by realizing $p$-adic $L$-functions as (essentially) the $Gamma$-transform of certain $p$-adic rational function measures. Shortly afterward, Gillard and Schneps independently adapted Sinnott's techniques to the case of $p$-adic $L$-functions associated to elliptic curves with complex multiplication (CM) by realizing these $p$-adic $L$-functions as $Gamma$-transforms of certain $p$-adic rational function measures. The results in the CM case give the vanishing of the Iwasawa $mu$-invariant for certain $mathbb{Z}_p$-extensions of imaginary quadratic fields constructed from torsion points of CM elliptic curves. In this thesis, I develop the theory of $p$-adic measures on $mathbb{Z}_p^d$, with particular interest given to the case of $d>1$. Although I introduce these measures within the context of $p$-adic integration, this study includes a strong emphasis on the interpretation of $p$-adic measures as $p$-adic power series. With this dual perspective, I describe $p$-adic analytic operations as maps on power series; the most important of these operations is the multivariate $Gamma$-transform on $p$-adic measures. This thesis gives new significance to product measures, and in particular to the use of product measures to construct measures on $mathbb{Z}_p^2$ from measures on $mathbb{Z}_p$. I introduce a subring of pseudo-polynomial measures on $mathbb{Z}_p^2$ which is closed under the standard operations on measures, including the $Gamma$-transform. I obtain results on the Iwasawa-invariants of such pseudo-polynomial measures, and use these results to deduce certain continuity results for the $Gamma$-transform. As an application, I establish the vanishing of the Iwasawa $mu$-invariant of Yager's two-variable $p$-adic $L$-function from measure theoretic considerations. / Dissertation/Thesis / Doctoral Dissertation Mathematics 2015