Approximate Relational Reasoning for Probabilistic Programs

La seguridad verificada es una metodología para demostrar propiedades de seguridad de los sistemas informáticos que se destaca por las altas garantías de corrección que provee. Los sistemas informáticos se modelan como programas probabilísticos y para probar que verifican una determinada propiedad de seguridad se utilizan técnicas rigurosas basadas en modelos matemáticos de los programas. En particular, la seguridad verificada promueve el uso de demostradores de teoremas interactivos o automáticos para construir demostraciones completamente formales cuya corrección es certificada mecánicamente (por ordenador). La seguridad verificada demostró ser una técnica muy efectiva para razonar sobre diversas nociones de seguridad en el área de criptografía. Sin embargo, no ha podido cubrir un importante conjunto de nociones de seguridad “aproximada”. La característica distintiva de estas nociones de seguridad es que se expresan como una condición de “similitud” entre las distribuciones de salida de dos programas probabilísticos y esta similitud se cuantifica usando alguna noción de distancia entre distribuciones de probabilidad. Este conjunto incluye destacadas nociones de seguridad de diversas áreas como la minería de datos privados, el análisis de flujo de información y la criptografía. Ejemplos representativos de estas nociones de seguridad son la indiferenciabilidad, que permite reemplazar un componente idealizado de un sistema por una implementación concreta (sin alterar significativamente sus propiedades de seguridad), o la privacidad diferencial, una noción de privacidad que ha recibido mucha atención en los últimos años y tiene como objetivo evitar la publicación datos confidenciales en la minería de datos. La falta de técnicas rigurosas que permitan verificar formalmente este tipo de propiedades constituye un notable problema abierto que tiene que ser abordado. En esta tesis introducimos varias lógicas de programa quantitativas para razonar sobre esta clase de propiedades de seguridad. Nuestra principal contribución teórica es una versión quantitativa de una lógica de Hoare relacional para programas probabilísticos. Las pruebas de correción de estas lógicas son completamente formalizadas en el asistente de pruebas Coq. Desarrollamos, además, una herramienta para razonar sobre propiedades de programas a través de estas lógicas extendiendo CertiCrypt, un framework para verificar pruebas de criptografía en Coq. Confirmamos la efectividad y aplicabilidad de nuestra metodología construyendo pruebas certificadas por ordendor de varios sistemas cuyo análisis estaba fuera del alcance de la seguridad verificada. Esto incluye, entre otros, una meta-construcción para diseñar funciones de hash “seguras” sobre curvas elípticas y algoritmos diferencialmente privados para varios problemas de optimización combinatoria de la literatura reciente. ABSTRACT The verified security methodology is an emerging approach to build high assurance proofs about security properties of computer systems. Computer systems are modeled as probabilistic programs and one relies on rigorous program semantics techniques to prove that they comply with a given security goal. In particular, it advocates the use of interactive theorem provers or automated provers to build fully formal machine-checked versions of these security proofs. The verified security methodology has proved successful in modeling and reasoning about several standard security notions in the area of cryptography. However, it has fallen short of covering an important class of approximate, quantitative security notions. The distinguishing characteristic of this class of security notions is that they are stated as a “similarity” condition between the output distributions of two probabilistic programs, and this similarity is quantified using some notion of distance between probability distributions. This class comprises prominent security notions from multiple areas such as private data analysis, information flow analysis and cryptography. These include, for instance, indifferentiability, which enables securely replacing an idealized component of system with a concrete implementation, and differential privacy, a notion of privacy-preserving data mining that has received a great deal of attention in the last few years. The lack of rigorous techniques for verifying these properties is thus an important problem that needs to be addressed. In this dissertation we introduce several quantitative program logics to reason about this class of security notions. Our main theoretical contribution is, in particular, a quantitative variant of a full-fledged relational Hoare logic for probabilistic programs. The soundness of these logics is fully formalized in the Coq proof-assistant and tool support is also available through an extension of CertiCrypt, a framework to verify cryptographic proofs in Coq. We validate the applicability of our approach by building fully machine-checked proofs for several systems that were out of the reach of the verified security methodology. These comprise, among others, a construction to build “safe” hash functions into elliptic curves and differentially private algorithms for several combinatorial optimization problems from the recent literature.

3D Frangi-based lung vessel enhancement filter penalizing airways

This paper describes a fully automatic simultaneous lung vessel and airway enhancement filter. The approach consists of a Frangi-based multiscale vessel enhancement filtering specifically designed for lung vessel and airway detection, where arteries and veins have high contrast with respect to the lung parenchyma, and airway walls are hollow tubular structures with a non negative response using the classical Frangi's filter. The features extracted from the Hessian matrix are used to detect centerlines and approximate walls of airways, decreasing the filter response in those areas by applying a penalty function to the vesselness measure. We validate the segmentation method in 20 CT scans with different pathological states within the VESSEL12 challenge framework. Results indicate that our approach obtains good results, decreasing the number of false positives in airway walls.

Noise-agnostic adaptive image filtering without training references on an evolvable hardware platform

One of the main concerns of evolvable and adaptive systems is the need of a training mechanism, which is normally done by using a training reference and a test input. The fitness function to be optimized during the evolution (training) phase is obtained by comparing the output of the candidate systems against the reference. The adaptivity that this type of systems may provide by re-evolving during operation is especially important for applications with runtime variable conditions. However, fully automated self-adaptivity poses additional problems. For instance, in some cases, it is not possible to have such reference, because the changes in the environment conditions are unknown, so it becomes difficult to autonomously identify which problem requires to be solved, and hence, what conditions should be representative for an adequate re-evolution. In this paper, a solution to solve this dependency is presented and analyzed. The system consists of an image filter application mapped on an evolvable hardware platform, able to evolve using two consecutive frames from a camera as both test and reference images. The system is entirely mapped in an FPGA, and native dynamic and partial reconfiguration is used for evolution. It is also shown that using such images, both of them being noisy, as input and reference images in the evolution phase of the system is equivalent or even better than evolving the filter with offline images. The combination of both techniques results in the completely autonomous, noise type/level agnostic filtering system without reference image requirement described along the paper.

On the approximate parametrization problem of algebraic curves.

The problem of parameterizing approximately algebraic curves and surfaces is an active research field, with many implications in practical applications. The problem can be treated locally or globally. We formally state the problem, in its global version for the case of algebraic curves (planar or spatial), and we report on some algorithms approaching it, as well as on the associated error distance analysis.

Laminar counterflow parallel-plate heat exchangers: Exact and approximate solutions

Multilayered, counterflow, parallel-plate heat exchangers are analyzed numerically and theoretically. The analysis, carried out for constant property fluids, considers a hydrodynamically developed laminar flow and neglects longitudinal conduction both in the fluid and in the plates. The solution for the temperature field involves eigenfunction expansions that can be solved in terms of Whittaker functions using standard symbolic algebra packages, leading to analytical expressions that provide the eigenvalues numerically. It is seen that the approximate solution obtained by retaining the first two modes in the eigenfunction expansion provides an accurate representation for the temperature away from the entrance regions, specially for long heat exchangers, thereby enabling simplified expressions for the wall and bulk temperatures, local heat-transfer rate, overall heat-transfer coefficient, and outlet bulk temperatures. The agreement between the numerical and theoretical results suggests the possibility of using the analytical solutions presented herein as benchmark problems for computational heat-transfer codes.

Comunicación intercomponente en ArchStudio 3.0: diseño del conector "message-filtering"

Tradicionalmente, el foco de atención en el desarrollo de una arquitectura software se ha centrado en los componentes, relegando a un segundo plano las formas de interacción entre estos componentes: los conectores. Sin embargo, para que un sistema funcione correctamente es necesario dedicar tanta atención a los conectores como a los componentes. En este trabajo presentamos un estudio sobre la herramienta ArchStudio 3.0. El análisis se ha centrado en las capacidades de dicha herramienta para soportar la comunicación entre componentes mediante paso de mensajes. Sobre dicha herramienta se han realizado correcciones en el código, se han rediseñado algunos de sus elementos para mejorar la eficiencia y se ha diseñado e implementado la política de filtrado C2 conocida como message filtering.

Rational Hausdorff Divisors: A New approach to the Approximate Parametrization of Curves.

When applying computational mathematics in practical applications, even though one may be dealing with a problem that can be solved algorithmically, and even though one has good algorithms to approach the solution, it can happen, and often it is the case, that the problem has to be reformulated and analyzed from a different computational point of view. This is the case of the development of approximate algorithms. This paper frames in the research area of approximate algebraic geometry and commutative algebra and, more precisely, on the problem of the approximate parametrization.

Depth filtering for auto-stereoscopic mobile devices

In this work we address a scenario where 3D content is transmitted to a mobile terminal with 3D display capabilities. We consider the use of 2D plus depth format to represent the 3D content and focus on the generation of synthetic views in the terminal. We evaluate different types of smoothing filters that are applied to depth maps with the aim of reducing the disoccluded regions. The evaluation takes into account the reduction of holes in the synthetic view as well as the presence of geometrical distortion caused by the smoothing operation. The selected filter has been included within an implemented module for the VideoLan Client (VLC) software in order to render 3D content from the 2D plus depth data format.

Aerodynamic database error filtering via high order singular value decomposition

Esta Tesis presenta un nuevo método para filtrar errores en bases de datos multidimensionales. Este método no precisa ninguna información a priori sobre la naturaleza de los errores. En concreto, los errrores no deben ser necesariamente pequeños, ni de distribución aleatoria ni tener media cero. El único requerimiento es que no estén correlados con la información limpia propia de la base de datos. Este nuevo método se basa en una extensión mejorada del método básico de reconstrucción de huecos (capaz de reconstruir la información que falta de una base de datos multidimensional en posiciones conocidas) inventado por Everson y Sirovich (1995). El método de reconstrucción de huecos mejorado ha evolucionado como un método de filtrado de errores de dos pasos: en primer lugar, (a) identifica las posiciones en la base de datos afectadas por los errores y después, (b) reconstruye la información en dichas posiciones tratando la información de éstas como información desconocida. El método resultante filtra errores O(1) de forma eficiente, tanto si son errores aleatorios como sistemáticos e incluso si su distribución en la base de datos está concentrada o esparcida por ella. Primero, se ilustra el funcionamiento delmétodo con una base de datosmodelo bidimensional, que resulta de la dicretización de una función transcendental. Posteriormente, se presentan algunos casos prácticos de aplicación del método a dos bases de datos tridimensionales aerodinámicas que contienen la distribución de presiones sobre un ala a varios ángulos de ataque. Estas bases de datos resultan de modelos numéricos calculados en CFD. ABSTRACT A method is presented to filter errors out in multidimensional databases. The method does not require any a priori information about the nature the errors. In particular, the errors need not to be small, neither random, nor exhibit zero mean. Instead, they are only required to be relatively uncorrelated to the clean information contained in the database. The method is based on an improved extension of a seminal iterative gappy reconstruction method (able to reconstruct lost information at known positions in the database) due to Everson and Sirovich (1995). The improved gappy reconstruction method is evolved as an error filtering method in two steps, since it is adapted to first (a) identify the error locations in the database and then (b) reconstruct the information in these locations by treating the associated data as gappy data. The resultingmethod filters out O(1) errors in an efficient fashion, both when these are random and when they are systematic, and also both when they concentrated and when they are spread along the database. The performance of the method is first illustrated using a two-dimensional toymodel database resulting fromdiscretizing a transcendental function and then tested on two CFD-calculated, three-dimensional aerodynamic databases containing the pressure coefficient on the surface of a wing for varying values of the angle of attack. A more general performance analysis of the method is presented with the intention of quantifying the randomness factor the method admits maintaining a correct performance and secondly, quantifying the size of error the method can detect. Lastly, some improvements of the method are proposed with their respective verification.

Approximate solution for frequency synchronization in a finite-size Kuramoto model

Peer reviewed

Perceptual learning reflects external noise filtering and internal noise reduction through channel reweighting

To investigate the nature of plasticity in the adult visual system, perceptual learning was measured in a peripheral orientation discrimination task with systematically varying amounts of external (environmental) noise. The signal contrasts required to achieve threshold were reduced by a factor or two or more after training at all levels of external noise. The strong quantitative regularities revealed by this novel paradigm ruled out changes in multiplicative internal noise, changes in transducer nonlinearites, and simple attentional tradeoffs. Instead, the regularities specify the mechanisms of perceptual learning at the behavioral level as a combination of external noise exclusion and stimulus enhancement via additive internal noise reduction. The findings also constrain the neural architecture of perceptual learning. Plasticity in the weights between basic visual channels and decision is sufficient to account for perceptual learning without requiring the retuning of visual mechanisms.

Complex mtDNA constitutes an approximate 620-kb insertion on Arabidopsis thaliana chromosome 2: Implication of potential sequencing errors caused by large-unit repeats

Previously conducted sequence analysis of Arabidopsis thaliana (ecotype Columbia-0) reported an insertion of 270-kb mtDNA into the pericentric region on the short arm of chromosome 2. DNA fiber-based fluorescence in situ hybridization analyses reveal that the mtDNA insert is 618 ± 42 kb, ≈2.3 times greater than that determined by contig assembly and sequencing analysis. Portions of the mitochondrial genome previously believed to be absent were identified within the insert. Sections of the mtDNA are repeated throughout the insert. The cytological data illustrate that DNA contig assembly by using bacterial artificial chromosomes tends to produce a minimal clone path by skipping over duplicated regions, thereby resulting in sequencing errors. We demonstrate that fiber-fluorescence in situ hybridization is a powerful technique to analyze large repetitive regions in the higher eukaryotic genomes and is a valuable complement to ongoing large genome sequencing projects.

Crop Phenology Estimation Using a Multitemporal Model and a Kalman Filtering Strategy

In this letter, a new approach for crop phenology estimation with remote sensing is presented. The proposed methodology is aimed to exploit tools from a dynamical system context. From a temporal sequence of images, a geometrical model is derived, which allows us to translate this temporal domain into the estimation problem. The evolution model in state space is obtained through dimensional reduction by a principal component analysis, defining the state variables, of the observations. Then, estimation is achieved by combining the generated model with actual samples in an optimal way using a Kalman filter. As a proof of concept, an example with results obtained with this approach over rice fields by exploiting stacks of TerraSAR-X dual polarization images is shown.

Power line interference filtering on surface electromyography based on the stationary wavelet packet transform

Power line interference is one of the main problems in surface electromyogram signals (EMG) analysis. In this work, a new method based on the stationary wavelet packet transform is proposed to estimate and remove this kind of noise from EMG data records. The performance has been quantitatively evaluated with synthetic noisy signals, obtaining good results independently from the signal to noise ratio (SNR). For the analyzed cases, the obtained results show that the correlation coefficient is around 0.99, the energy respecting to the pure EMG signal is 98–104%, the SNR is between 16.64 and 20.40 dB and the mean absolute error (MAE) is in the range of −69.02 and −65.31 dB. It has been also applied on 18 real EMG signals, evaluating the percentage of energy respecting to the noisy signals. The proposed method adjusts the reduction level to the amplitude of each harmonic present in the analyzed noisy signals (synthetic and real), reducing the harmonics with no alteration of the desired signal.

SeismicWaveTool: Continuous and discrete wavelet analysis and filtering for multichannel seismic data

A MATLAB-based computer code has been developed for the simultaneous wavelet analysis and filtering of multichannel seismic data. The considered time–frequency transforms include the continuous wavelet transform, the discrete wavelet transform and the discrete wavelet packet transform. The developed approaches provide a fast and precise time–frequency examination of the seismograms at different frequency bands. Moreover, filtering methods for noise, transients or even baseline removal, are implemented. The primary motivation is to support seismologists with a user-friendly and fast program for the wavelet analysis, providing practical and understandable results.