-
Nanopass Back-Translation of Call-Return Trees for Mechanized Secure Compilation Proofs
Authors:
Jérémy Thibault,
Joseph Lenormand,
Catalin Hritcu
Abstract:
Researchers aim to build secure compilation chains enforcing that if there is no attack a source context can mount against a source program then there is also no attack an adversarial target context can mount against the compiled program. Proving that these compilation chains are secure is, however, challenging, and involves a non-trivial back-translation step: for any attack a target context moun…
▽ More
Researchers aim to build secure compilation chains enforcing that if there is no attack a source context can mount against a source program then there is also no attack an adversarial target context can mount against the compiled program. Proving that these compilation chains are secure is, however, challenging, and involves a non-trivial back-translation step: for any attack a target context mounts against the compiled program one has to exhibit a source context mounting the same attack against the source program. We describe a novel back-translation technique, which results in simpler proofs that can be more easily mechanized in a proof assistant. Given a finite set of finite trace prefixes, capturing the interaction recorded during an attack between a target context and the compiled program, we build a call-return tree that we back-translate into a source context producing the same trace prefixes. We use state in the generated source context to record the current location in the call-return tree. The back-translation is done in several small steps, each adding to the tree new information describing how the location should change depending on how the context regains control. To prove this back-translation correct we give semantics to every intermediate call-return tree language, using ghost state to store information and explicitly enforce execution invariants. We prove several small forward simulations, basically seeing the back-translation as a verified nanopass compiler. Thanks to this modular structure, we are able to mechanize this complex back-translation and its correctness proof in the Rocq prover without too much effort.
△ Less
Submitted 11 April, 2025; v1 submitted 25 March, 2025;
originally announced March 2025.
-
SECOMP: Formally Secure Compilation of Compartmentalized C Programs
Authors:
Jérémy Thibault,
Roberto Blanco,
Dongjae Lee,
Sven Argo,
Arthur Azevedo de Amorim,
Aïna Linn Georges,
Catalin Hritcu,
Andrew Tolmach
Abstract:
Undefined behavior in C often causes devastating security vulnerabilities. One practical mitigation is compartmentalization, which allows developers to structure large programs into mutually distrustful compartments with clearly specified privileges and interactions. In this paper we introduce SECOMP, a compiler for compartmentalized C code that comes with machine-checked proofs guaranteeing that…
▽ More
Undefined behavior in C often causes devastating security vulnerabilities. One practical mitigation is compartmentalization, which allows developers to structure large programs into mutually distrustful compartments with clearly specified privileges and interactions. In this paper we introduce SECOMP, a compiler for compartmentalized C code that comes with machine-checked proofs guaranteeing that the scope of undefined behavior is restricted to the compartments that encounter it and become dynamically compromised. These guarantees are formalized as the preservation of safety properties against adversarial contexts, a secure compilation criterion similar to full abstraction, and this is the first time such a strong criterion is proven for a mainstream programming language. To achieve this we extend the languages of the CompCert verified C compiler with isolated compartments that can only interact via procedure calls and returns, as specified by cross-compartment interfaces. We adapt the passes and optimizations of CompCert as well as their correctness proofs to this compartment-aware setting. We then use compiler correctness as an ingredient in a larger secure compilation proof that involves several proof engineering novelties, needed to scale formally secure compilation up to a C compiler.
△ Less
Submitted 1 January, 2025; v1 submitted 29 January, 2024;
originally announced January 2024.
-
Three-axis torque investigation of interfacial exchange coupling in a NiFe/CoO bilayer micromagnetic disk
Authors:
M. G. Dunsmore,
J. A. Thibault,
K. R. Fast,
V. T. K. Sauer,
J. E. Losby,
Z. Diao,
M. Belov,
M. R. Freeman
Abstract:
Micrometer diameter bilayers of NiFe (permalloy, Py) and cobalt oxide (CoO) deposited on nanomechanical resonators were used to investigate exchange bias effects. The mechanical compliances of two resonator axes were enhanced by severing one torsion arm, resulting in a unique three-axis resonator that responds resonantly to torques generated by a three-axis RF field. Our technique permits simultan…
▽ More
Micrometer diameter bilayers of NiFe (permalloy, Py) and cobalt oxide (CoO) deposited on nanomechanical resonators were used to investigate exchange bias effects. The mechanical compliances of two resonator axes were enhanced by severing one torsion arm, resulting in a unique three-axis resonator that responds resonantly to torques generated by a three-axis RF field. Our technique permits simultaneous measurement of three orthogonal torque components. Measurements of the anisotropies associated with interfacial exchange coupling effects have been made. At cryogenic temperatures, observations of shifted linear hysteresis loops confirmed the presence of exchange bias from the Py/CoO interface. An in-plane rotating DC bias field was used to probe in-plane anisotropies through the out-of-plane torque. Training effects in the rotational hysteresis data were observed and showed that features due to interfacial coupling did not diminish irrespective of substantial training of the unidirectional anisotropy. The data from the rotational hysteresis loops were fit with parameters from a macrospin solution to the Landau-Lifshitz-Gilbert equation. Each parameter of the exchange bias model accounts for specific features of the rotational loop.
△ Less
Submitted 4 February, 2022;
originally announced February 2022.
-
SecurePtrs: Proving Secure Compilation with Data-Flow Back-Translation and Turn-Taking Simulation
Authors:
Akram El-Korashy,
Roberto Blanco,
Jérémy Thibault,
Adrien Durier,
Deepak Garg,
Catalin Hritcu
Abstract:
Proving secure compilation of partial programs typically requires back-translating an attack against the compiled program to an attack against the source program. To prove back-translation, one can syntactically translate the target attacker to a source one -- i.e., syntax-directed back-translation -- or show that the interaction traces of the target attacker can also be emitted by source attacker…
▽ More
Proving secure compilation of partial programs typically requires back-translating an attack against the compiled program to an attack against the source program. To prove back-translation, one can syntactically translate the target attacker to a source one -- i.e., syntax-directed back-translation -- or show that the interaction traces of the target attacker can also be emitted by source attackers -- i.e., trace-directed back-translation.
Syntax-directed back-translation is not suitable when the target attacker may use unstructured control flow that the source language cannot directly represent. Trace-directed back-translation works with such syntactic dissimilarity because only the external interactions of the target attacker have to be mimicked in the source, not its internal control flow. Revealing only external interactions is, however, inconvenient when sharing memory via unforgeable pointers, since information about shared pointers stashed in private memory is not present on the trace. This made prior proofs unnecessarily complex, since the generated attacker had to instead stash all reachable pointers.
In this work, we introduce more informative *data-flow traces*, combining the best of syntax- and trace-directed back-translation in a simpler technique that handles both syntactic dissimilarity and memory sharing well, and that is proved correct in Coq. Additionally, we develop a novel *turn-taking simulation* relation and use it to prove a recomposition lemma, which is key to reusing compiler correctness in such secure compilation proofs. We are the first to mechanize such a recomposition lemma in the presence of memory sharing.
We use these two innovations in a secure compilation proof for a code generation compiler pass between a source language with structured control flow and a target language with unstructured control flow, both with safe pointers and components.
△ Less
Submitted 3 June, 2022; v1 submitted 4 October, 2021;
originally announced October 2021.
-
Simultaneous three-axis torque measurements of micromagnetism
Authors:
K. R. Fast,
J. A. Thibault,
V. T. K. Sauer,
M. G. Dunsmore,
A. Kav,
J. E. Losby,
Z. Diao,
E. J. Luber,
M. Belov,
M. R. Freeman
Abstract:
Measurements of magnetic torque are most commonly preformed about a single axis or component of torque. Such measurements are very useful for hysteresis measurements of thin film structures in particular, where high shape anisotropy yields a near-proportionality of in-plane magnetic moment and the magnetic torque along the perpendicular in-plane axis. A technique to measure the full magnetic torqu…
▽ More
Measurements of magnetic torque are most commonly preformed about a single axis or component of torque. Such measurements are very useful for hysteresis measurements of thin film structures in particular, where high shape anisotropy yields a near-proportionality of in-plane magnetic moment and the magnetic torque along the perpendicular in-plane axis. A technique to measure the full magnetic torque vector (three orthogonal torque components) on micro- and nano-scale magnetic materials is introduced. The method is demonstrated using a modified, single-paddle silicon-on-insulator resonant torque sensor. The mechanical compliances to all three orthogonal torque components are maximized by clamping the sensor at a single point. Mechanically-resonant AC torques are driven by an RF field containing a frequency component for each fundamental torsional mode of the device, and the resulting displacements read out through optical position-sensitive detection. The measurements are compared with micromagnetic simulations of the mechanical torque to augment the interpretation of the signals. As an application example, simultaneous observations of hysteresis in the net magnetization along with the field-dependent in-plane anisotropy is highly beneficial for studies of exchange bias.
△ Less
Submitted 2 November, 2020;
originally announced November 2020.
-
Ordered Functional Decision Diagrams: A Functional Semantics For Binary Decision Diagrams
Authors:
Joan Thibault,
Khalil Ghorbal
Abstract:
We introduce a novel framework, termed $λ$DD, that revisits Binary Decision Diagrams from a purely functional point of view. The framework allows to classify the already existing variants, including the most recent ones like Chain-DD and ESRBDD, as implementations of a special class of ordered models. We enumerate, in a principled way, all the models of this class and isolate its most expressive m…
▽ More
We introduce a novel framework, termed $λ$DD, that revisits Binary Decision Diagrams from a purely functional point of view. The framework allows to classify the already existing variants, including the most recent ones like Chain-DD and ESRBDD, as implementations of a special class of ordered models. We enumerate, in a principled way, all the models of this class and isolate its most expressive model. This new model, termed $λ$DD-O-NUCX, is suitable for both dense and sparse Boolean functions, and is moreover invariant by negation. The canonicity of $λ$DD-O-NUCX is formally verified using the Coq proof assistant. We furthermore give bounds on the size of the different diagrams: the potential gain achieved by more expressive models can be at most linear in the number of variables n.
△ Less
Submitted 21 July, 2020; v1 submitted 20 March, 2020;
originally announced March 2020.
-
Trace-Relating Compiler Correctness and Secure Compilation
Authors:
Carmine Abate,
Roberto Blanco,
Stefan Ciobaca,
Adrien Durier,
Deepak Garg,
Catalin Hritcu,
Marco Patrignani,
Éric Tanter,
Jérémy Thibault
Abstract:
Compiler correctness is, in its simplest form, defined as the inclusion of the set of traces of the compiled program into the set of traces of the original program, which is equivalent to the preservation of all trace properties. Here traces collect, for instance, the externally observable events of each execution. This definition requires, however, the set of traces of the source and target langu…
▽ More
Compiler correctness is, in its simplest form, defined as the inclusion of the set of traces of the compiled program into the set of traces of the original program, which is equivalent to the preservation of all trace properties. Here traces collect, for instance, the externally observable events of each execution. This definition requires, however, the set of traces of the source and target languages to be exactly the same, which is not the case when the languages are far apart or when observations are fine-grained. To overcome this issue, we study a generalized compiler correctness definition, which uses source and target traces drawn from potentially different sets and connected by an arbitrary relation. We set out to understand what guarantees this generalized compiler correctness definition gives us when instantiated with a non-trivial relation on traces. When this trace relation is not equality, it is no longer possible to preserve the trace properties of the source program unchanged. Instead, we provide a generic characterization of the target trace property ensured by correctly compiling a program that satisfies a given source property, and dually, of the source trace property one is required to show in order to obtain a certain target property for the compiled code. We show that this view on compiler correctness can naturally account for undefined behavior, resource exhaustion, different source and target values, side-channels, and various abstraction mismatches. Finally, we show that the same generalization also applies to many secure compilation definitions, which characterize the protection of a compiled program against linked adversarial code.
△ Less
Submitted 23 February, 2020; v1 submitted 11 July, 2019;
originally announced July 2019.
-
2.5D Deep Learning for CT Image Reconstruction using a Multi-GPU implementation
Authors:
Amirkoushyar Ziabari,
Dong Hye Ye,
Somesh Srivastava,
Ken D. Sauer,
Jean-Baptiste Thibault,
Charles A. Bouman
Abstract:
While Model Based Iterative Reconstruction (MBIR) of CT scans has been shown to have better image quality than Filtered Back Projection (FBP), its use has been limited by its high computational cost. More recently, deep convolutional neural networks (CNN) have shown great promise in both denoising and reconstruction applications. In this research, we propose a fast reconstruction algorithm, which…
▽ More
While Model Based Iterative Reconstruction (MBIR) of CT scans has been shown to have better image quality than Filtered Back Projection (FBP), its use has been limited by its high computational cost. More recently, deep convolutional neural networks (CNN) have shown great promise in both denoising and reconstruction applications. In this research, we propose a fast reconstruction algorithm, which we call Deep Learning MBIR (DL-MBIR), for approximating MBIR using a deep residual neural network. The DL-MBIR method is trained to produce reconstructions that approximate true MBIR images using a 16 layer residual convolutional neural network implemented on multiple GPUs using Google Tensorflow. In addition, we propose 2D, 2.5D and 3D variations on the DL-MBIR method and show that the 2.5D method achieves similar quality to the fully 3D method, but with reduced computational cost.
△ Less
Submitted 20 December, 2018;
originally announced December 2018.
-
Model Based Iterative Reconstruction With Spatially Adaptive Sinogram Weights for Wide-Cone Cardiac CT
Authors:
Amirkoushyar Ziabari,
Dong Hye Ye,
Lin Fu,
Somesh Srivastava,
Ken D. Sauer,
Jean-Baptist Thibault,
Charles A. Bouman
Abstract:
With the recent introduction of CT scanners with large cone angles, wide coverage detectors now provide a desirable scanning platform for cardiac CT that allows whole heart imaging in a single rotation. On these scanners, while half-scan data is strictly sufficient to produce images with the best temporal resolution, acquiring a full 360 degree rotation worth of data is beneficial for wide-cone im…
▽ More
With the recent introduction of CT scanners with large cone angles, wide coverage detectors now provide a desirable scanning platform for cardiac CT that allows whole heart imaging in a single rotation. On these scanners, while half-scan data is strictly sufficient to produce images with the best temporal resolution, acquiring a full 360 degree rotation worth of data is beneficial for wide-cone image reconstruction at negligible additional radiation dose. Applying Model-Based Iterative Reconstruction (MBIR) algorithm to the heart has shown to yield significant enhancement in image quality for cardiac CT. But imaging the heart in large cone angle geometry leads to apparently conflicting data usage considerations. On the one hand, in addition to using the fastest available scanner rotation speed, a minimal complete data set of 180 degrees plus the fan angle is typically used to minimize both cardiac and respiratory motion. On the other hand, a full 360 degree acquisition helps better handle the challenges of missing frequencies and incomplete projections associated with wide-cone half-scan data acquisition. In this paper, we develop a Spatially Adaptive sinogram Weights MBIR algorithm (SAW-MBIR) that is designed to achieve the benefits of both half and full-scan reconstructions in order to maximize temporal resolution over the heart region while providing stable results over the whole volume covered with the wide-area detector. Spatially-adaptive sinogram weights applied to each projection measurement in SAW-MBIR are designed to selectively perform backprojection from the full and half-scan portion of the sinogram based on both projection angle and reconstructed voxel location. We demonstrate with experimental results of SAW-MBIR applied to whole-heart cardiac CT clinical data that overall temporal resolution matches half-scan while full volume image quality is on par with full-scan MBIR.
△ Less
Submitted 20 December, 2018;
originally announced December 2018.
-
Journey Beyond Full Abstraction: Exploring Robust Property Preservation for Secure Compilation
Authors:
Carmine Abate,
Roberto Blanco,
Deepak Garg,
Catalin Hritcu,
Marco Patrignani,
Jérémy Thibault
Abstract:
(CROPPED TO FIT IN ARXIV'S SILLY LIMIT. SEE PDF FOR COMPLETE ABSTRACT.)
We are the first to thoroughly explore a large space of formal secure compilation criteria based on robust property preservation, i.e., the preservation of properties satisfied against arbitrary adversarial contexts. We study robustly preserving various classes of trace properties such as safety, of hyperproperties such as n…
▽ More
(CROPPED TO FIT IN ARXIV'S SILLY LIMIT. SEE PDF FOR COMPLETE ABSTRACT.)
We are the first to thoroughly explore a large space of formal secure compilation criteria based on robust property preservation, i.e., the preservation of properties satisfied against arbitrary adversarial contexts. We study robustly preserving various classes of trace properties such as safety, of hyperproperties such as noninterference, and of relational hyperproperties such as trace equivalence. This leads to many new secure compilation criteria, some of which are easier to practically achieve and prove than full abstraction, and some of which provide strictly stronger security guarantees. For each of the studied criteria we propose an equivalent "property-free" characterization that clarifies which proof techniques apply. For relational properties and hyperproperties, which relate the behaviors of multiple programs, our formal definitions of the property classes themselves are novel. We order our criteria by their relative strength and show several collapses and separation results. Finally, we adapt existing proof techniques to show that even the strongest of our secure compilation criteria, the robust preservation of all relational hyperproperties, is achievable for a simple translation from a statically typed to a dynamically typed language.
△ Less
Submitted 17 May, 2019; v1 submitted 12 July, 2018;
originally announced July 2018.
-
Laning and Clustering Transitions in Driven Binary Active Matter Systems
Authors:
C. Reichhardt,
J. Thibault,
S. Papanikolaou,
C. J. O. Reichhardt
Abstract:
It is well known that a binary system of non-active disks that experience driving in opposite directions exhibits jammed, phase separated, disordered, and laning states. In active matter systems, such as a crowd of pedestrians, driving in opposite directions is common and relevant, especially in conditions which are characterized by high pedestrian density and emergency. In such cases, the transit…
▽ More
It is well known that a binary system of non-active disks that experience driving in opposite directions exhibits jammed, phase separated, disordered, and laning states. In active matter systems, such as a crowd of pedestrians, driving in opposite directions is common and relevant, especially in conditions which are characterized by high pedestrian density and emergency. In such cases, the transition from laning to disordered states may be associated with the onset of a panic state. We simulate a laning system containing active disks that obey run-and-tumble dynamics, and we measure the drift mobility and structure as a function of run length, disk density, and drift force. The activity of each disk can be quantified based on the correlation timescale of the velocity vector. We find that in some cases, increasing the activity can increase the system mobility by breaking up jammed configurations; however, an activity level that is too high can reduce the mobility by increasing the probability of disk-disk collisions. In the laning state, the increase of activity induces a sharp transition to a disordered strongly fluctuating state with reduced mobility. We identify a novel drive-induced clustered laning state that remains stable even at densities below the activity-induced clustering transition of the undriven system.
△ Less
Submitted 17 May, 2018;
originally announced May 2018.
-
When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise
Authors:
Carmine Abate,
Arthur Azevedo de Amorim,
Roberto Blanco,
Ana Nora Evans,
Guglielmo Fachini,
Catalin Hritcu,
Théo Laurent,
Benjamin C. Pierce,
Marco Stronati,
Jérémy Thibault,
Andrew Tolmach
Abstract:
We propose a new formal criterion for evaluating secure compilation schemes for unsafe languages, expressing end-to-end security guarantees for software components that may become compromised after encountering undefined behavior---for example, by accessing an array out of bounds.
Our criterion is the first to model dynamic compromise in a system of mutually distrustful components with clearly s…
▽ More
We propose a new formal criterion for evaluating secure compilation schemes for unsafe languages, expressing end-to-end security guarantees for software components that may become compromised after encountering undefined behavior---for example, by accessing an array out of bounds.
Our criterion is the first to model dynamic compromise in a system of mutually distrustful components with clearly specified privileges. It articulates how each component should be protected from all the others---in particular, from components that have encountered undefined behavior and become compromised. Each component receives secure compilation guarantees---in particular, its internal invariants are protected from compromised components---up to the point when this component itself becomes compromised, after which we assume an attacker can take complete control and use this component's privileges to attack other components. More precisely, a secure compilation chain must ensure that a dynamically compromised component cannot break the safety properties of the system at the target level any more than an arbitrary attacker-controlled component (with the same interface and privileges, but without undefined behaviors) already could at the source level.
To illustrate the model, we construct a secure compilation chain for a small unsafe language with buffers, procedures, and components, targeting a simple abstract machine with built-in compartmentalization. We give a machine-checked proof in Coq that this compiler satisfies our secure compilation criterion. Finally, we show that the protection guarantees offered by the compartmentalized abstract machine can be achieved at the machine-code level using either software fault isolation or a tag-based reference monitor.
△ Less
Submitted 29 November, 2019; v1 submitted 2 February, 2018;
originally announced February 2018.
-
Brittle to Quasi-Brittle Transition and Crack Initiation Precursors in Disordered Crystals
Authors:
S. Papanikolaou,
J. Thibault,
C. Woodward,
P. Shanthraj,
F. Roters
Abstract:
Crack initiation emerges due to a combination of elasticity, plasticity, and disorder, and it is heavily dependent on the material's microstructural details. In this paper, we investigate brittle metals with coarse-grained, microstructural disorder that could originate in a material's manufacturing process, such as alloying. As an investigational tool, we consider crack initiation from a surface,…
▽ More
Crack initiation emerges due to a combination of elasticity, plasticity, and disorder, and it is heavily dependent on the material's microstructural details. In this paper, we investigate brittle metals with coarse-grained, microstructural disorder that could originate in a material's manufacturing process, such as alloying. As an investigational tool, we consider crack initiation from a surface, ellipsoidal notch: As the radius of curvature at the notch increases, there is a dynamic transition from notch-induced crack initiation to bulk-disorder crack nucleation. We perform extensive and realistic simulations using a phase-field approach coupled to crystal plasticity. Furthermore, the microstructural disorder and notch width are varied in order to study the transition. We identify this transition for various disorder strengths in terms of the damage evolution. Above the transition, we identify detectable precursors to crack initiation that we quantify in terms of the expected stress drops during mode I fracture loading. We discuss ways to observe and analyze this brittle to quasi-brittle transition in experiments.
△ Less
Submitted 13 July, 2017;
originally announced July 2017.
-
Experimental evidence for field induced emergent clock anisotropies in the XY pyrochlore Er$_2$Ti$_2$O$_7$
Authors:
J. Gaudet,
A. M. Hallas,
J. Thibault,
N. P. Butch,
H. A. Dabkowska,
B. D. Gaulin
Abstract:
The XY pyrochlore antiferromagnet Er$_2$Ti$_2$O$_7$ exhibits a rare case of $Z_6$ discrete symmetry breaking in its $ψ_2$ magnetic ground state. Despite being well-studied theoretically, systems with high discrete symmetry breakings are uncommon in nature and, thus, Er$_2$Ti$_2$O$_7$ provides an experimental playground for the study of broken $Z_n$ symmetry, for $n>2$. A recent theoretical work ex…
▽ More
The XY pyrochlore antiferromagnet Er$_2$Ti$_2$O$_7$ exhibits a rare case of $Z_6$ discrete symmetry breaking in its $ψ_2$ magnetic ground state. Despite being well-studied theoretically, systems with high discrete symmetry breakings are uncommon in nature and, thus, Er$_2$Ti$_2$O$_7$ provides an experimental playground for the study of broken $Z_n$ symmetry, for $n>2$. A recent theoretical work examined the effect of a magnetic field on a pyrochlore lattice with broken $Z_6$ symmetry and applied it to Er$_2$Ti$_2$O$_7$. This study predicted multiple domain transitions depending on the crystallographic orientation of the magnetic field, inducing rich and controllable magnetothermodynamic behavior. In this work, we present neutron scattering measurements on Er$_2$Ti$_2$O$_7$ with a magnetic field applied along the [001] and [111] directions, and provide the first experimental observation of these exotic domain transitions. In a [001] field, we observe a $ψ_2$ to $ψ_3$ transition at a critical field of 0.18$\pm$0.05T. We are thus able to extend the concept of the spin-flop transition, which has long been observed in Ising systems, to higher discrete $Z_n$ symmetries. In a [111] field, we observe a series of domain-based phase transitions for fields of 0.15$\pm$0.03T and 0.40$\pm$0.03T. We show that these field-induced transitions are consistent with the emergence of two-fold, three-fold and possibly six-fold Zeeman terms. Considering all the possible $ψ_2$ and $ψ_3$ domains, these Zeeman terms can be mapped onto an analog clock - exemplifying a literal clock anisotropy. Lastly, our quantitative analysis of the [001] domain transition in Er$_2$Ti$_2$O$_7$ is consistent with order-by-disorder as the dominant ground state selection mechanism.
△ Less
Submitted 11 January, 2017;
originally announced January 2017.
-
A Gaussian Mixture MRF for Model-Based Iterative Reconstruction with Applications to Low-Dose X-ray CT
Authors:
Ruoqiao Zhang,
Dong Hye Ye,
Debashish Pal,
Jean-Baptiste Thibault,
Ken D. Sauer,
Charles A. Bouman
Abstract:
Markov random fields (MRFs) have been widely used as prior models in various inverse problems such as tomographic reconstruction. While MRFs provide a simple and often effective way to model the spatial dependencies in images, they suffer from the fact that parameter estimation is difficult. In practice, this means that MRFs typically have very simple structure that cannot completely capture the s…
▽ More
Markov random fields (MRFs) have been widely used as prior models in various inverse problems such as tomographic reconstruction. While MRFs provide a simple and often effective way to model the spatial dependencies in images, they suffer from the fact that parameter estimation is difficult. In practice, this means that MRFs typically have very simple structure that cannot completely capture the subtle characteristics of complex images.
In this paper, we present a novel Gaussian mixture Markov random field model (GM-MRF) that can be used as a very expressive prior model for inverse problems such as denoising and reconstruction. The GM-MRF forms a global image model by merging together individual Gaussian-mixture models (GMMs) for image patches. In addition, we present a novel analytical framework for computing MAP estimates using the GM-MRF prior model through the construction of surrogate functions that result in a sequence of quadratic optimizations. We also introduce a simple but effective method to adjust the GM-MRF so as to control the sharpness in low- and high-contrast regions of the reconstruction separately. We demonstrate the value of the model with experiments including image denoising and low-dose CT reconstruction.
△ Less
Submitted 13 June, 2016; v1 submitted 12 May, 2016;
originally announced May 2016.
-
On the Finite-Dimensional Irreducible Representations of PSL2(Z)
Authors:
Melinda G. Moran,
Matthew J. Thibault
Abstract:
We classify up to equivalence all finite-dimensional irreducible representations of PSL2(Z) whose restriction to the commutator subgroup is diagonalizable.
We classify up to equivalence all finite-dimensional irreducible representations of PSL2(Z) whose restriction to the commutator subgroup is diagonalizable.
△ Less
Submitted 19 July, 2005;
originally announced July 2005.
