A robustness verification system for mobile phone authentication based on gestures using Linear Discriminant Analysis

This article evaluates an authentication technique for mobiles based on gestures. Users create a remindful identifying gesture to be considered as their in-air signature. This work analyzes a database of 120 gestures of different vulnerability, obtaining an Equal Error Rate (EER) of 9.19% when robustness of gestures is not verified. Most of the errors in this EER come from very simple and easily forgeable gestures that should be discarded at enrollment phase. Therefore, an in-air signature robustness verification system using Linear Discriminant Analysis is proposed to infer automatically whether the gesture is secure or not. Different configurations have been tested obtaining a lowest EER of 4.01% when 45.02% of gestures were discarded, and an optimal compromise of EER of 4.82% when 19.19% of gestures were automatically rejected.

Propuesta, implementación y evaluación de la biometría de firma en el aire como sistema de verificación en teléfonos móviles

En esta tesis doctoral se propone una técnica biométrica de verificación en teléfonos móviles consistente en realizar una firma en el aire con la mano que sujeta el teléfono móvil. Los acelerómetros integrados en el dispositivo muestrean las aceleraciones del movimiento de la firma en el aire, generando tres señales temporales que pueden utilizarse para la verificación del usuario. Se proponen varios enfoques para la implementación del sistema de verificación, a partir de los enfoques más utilizados en biometría de firma manuscrita: correspondencia de patrones, con variantes de los algoritmos de Needleman-Wusch (NW) y Dynamic Time Warping (DTW), modelos ocultos de Markov (HMM) y clasificador estadístico basado en Máquinas de Vector Soporte (SVM). Al no existir bases de datos públicas de firmas en el aire y con el fin de evaluar los métodos propuestos en esta tesis doctoral, se han capturado dos con distintas características; una con falsificaciones reales a partir del estudio de las grabaciones de usuarios auténticos y otra con muestras de usuarios obtenidas en diferentes sesiones a lo largo del tiempo. Utilizando estas bases de datos se han evaluado una gran cantidad de algoritmos para implementar un sistema de verificación basado en firma en el aire. Esta evaluación se ha realizado de acuerdo con el estándar ISO/IEC 19795, añadiendo el caso de verificación en mundo abierto no incluido en la norma. Además, se han analizado las características que hacen que una firma sea suficientemente segura. Por otro lado, se ha estudiado la permanencia de las firmas en el aire a lo largo del tiempo, proponiendo distintos métodos de actualización, basados en una adaptación dinámica del patrón, para mejorar su rendimiento. Finalmente, se ha implementado un prototipo de la técnica de firma en el aire para teléfonos Android e iOS. Los resultados de esta tesis doctoral han tenido un gran impacto, generando varias publicaciones en revistas internacionales, congresos y libros. La firma en el aire ha sido nombrada también en varias revistas de divulgación, portales de noticias Web y televisión. Además, se han obtenido varios premios en competiciones de ideas innovadoras y se ha firmado un acuerdo de explotación de la tecnología con una empresa extranjera. ABSTRACT This thesis proposes a biometric verification technique on mobile phones consisting on making a signature in the air with the hand holding a mobile phone. The accelerometers integrated in the device capture the movement accelerations, generating three temporal signals that can be used for verification. This thesis suggests several approaches for implementing the verification system, based on the most widely used approaches in handwritten signature biometrics: template matching, with a lot of variations of the Needleman- Wusch (NW) and Dynamic Time Warping (DTW) algorithms, Hidden Markov Models (HMM) and Supported Vector Machines (SVM). As there are no public databases of in-air signatures and with the aim of assessing the proposed methods, there have been captured two databases; one. with real falsification attempts from the study of recordings captured when genuine users made their signatures in front of a camera, and other, with samples obtained in different sessions over a long period of time. These databases have been used to evaluate a lot of algorithms in order to implement a verification system based on in-air signatures. This evaluation has been conducted according to the standard ISO/IEC 19795, adding the open-set verification scenario not included in the norm. In addition, the characteristics of a secure signature are also investigated, as well as the permanence of in-air signatures over time, proposing several updating strategies to improve its performance. Finally, a prototype of in-air signature has been developed for iOS and Android phones. The results of this thesis have achieved a high impact, publishing several articles in SCI journals, conferences and books. The in-air signature deployed in this thesis has been also referred in numerous media. Additionally, this technique has won several awards in the entrepreneurship field and also an exploitation agreement has been signed with a foreign company.

Experimentel ADS-B based surveillance

This paper describes an ADS-B implementation in air-to-air and ground based experimental surveillance within a prototype ATM system. The relations between airborne and ground systems related to surveillance are detailed, and the prototype surveillance systems and their algorithms described. Their performance is analysed, based both on simulated and real data.

Lateral impact sensor for measuring firmness of fruits in an experimental packing line.

Different parameters are used to quantify the maturity of fruits at or near harvest (shape, color, flesh texture and internal composition). Flesh firmness is a critical handling parameter for fruits such as peach, pear and apple. Results of previous studies conducted by different researchers have shown that impact techniques can be used to evaluate firmness of fruits. A prototype impact system for firmness sorting of fruits was developed by Chen and Ruiz-Altisent (Chen et al, 1996). This sensor was mounted and tested successfully on a 3 m section of a commercial conveyor belt (Chen et al, 1998). This is a further development of the on-line impact system for firmness sorting of fruits. The design of the sensor has been improved and it has been mounted on a experimental fruit packing line (Ortiz-Cañavate et al 1999).

Formal verification of safety protocol in train control system

In order to satisfy the safety-critical requirements, the train control system (TCS) often employs a layered safety communication protocol to provide reliable services. However, both description and verification of the safety protocols may be formidable due to the system complexity. In this paper, interface automata (IA) are used to describe the safety service interface behaviors of safety communication protocol. A formal verification method is proposed to describe the safety communication protocols using IA and translate IA model into PROMELA model so that the protocols can be verified by the model checker SPIN. A case study of using this method to describe and verify a safety communication protocol is included. The verification results illustrate that the proposed method is effective to describe the safety protocols and verify deadlocks, livelocks and several mandatory consistency properties. A prototype of safety protocols is also developed based on the presented formally verifying method.

Integrated program debugging, verification, and optimization using abstract interpretation (and the Ciao system preprocessor)

The technique of Abstract Interpretation has allowed the development of very sophisticated global program analyses which are at the same time provably correct and practical. We present in a tutorial fashion a novel program development framework which uses abstract interpretation as a fundamental tool. The framework uses modular, incremental abstract interpretation to obtain information about the program. This information is used to validate programs, to detect bugs with respect to partial specifications written using assertions (in the program itself and/or in system libraries), to generate and simplify run-time tests, and to perform high-level program transformations such as multiple abstract specialization, parallelization, and resource usage control, all in a provably correct way. In the case of validation and debugging, the assertions can refer to a variety of program points such as procedure entry, procedure exit, points within procedures, or global computations. The system can reason with much richer information than, for example, traditional types. This includes data structure shape (including pointer sharing), bounds on data structure sizes, and other operational variable instantiation properties, as well as procedure-level properties such as determinacy, termination, nonfailure, and bounds on resource consumption (time or space cost). CiaoPP, the preprocessor of the Ciao multi-paradigm programming system, which implements the described functionality, will be used to illustrate the fundamental ideas.

ITER fast plan system controlle prototype based on PXI platform

Presentación de una ponencia invitada en el 4th Annual Pan-European Big Physics Symposium

ITER fast plant system controller prototype based on PXIe platform

The ITER CODAC design identifies slow and fast plant system controllers (PSC). The gast OSCs are based on embedded technologies, permit sampling rates greater than 1 KHz, meet stringent real-time requirements, and will be devoted to data acquisition tasks and control purposes. CIEMAT and UPM have implemented a prototype of a fast PSC based on commercial off-the-shelf (COTS) technologies with PXI hardware and software based on EPICS

NetCDF based data archiving system applied to ITER Fast Plant System Control prototype

EURATOM/CIEMAT and Technical University of Madrid (UPM) have been involved in the development of a FPSC [1] (Fast Plant System Control) prototype for ITER, based on PXIe (PCI eXtensions for Instrumentation). One of the main focuses of this project has been data acquisition and all the related issues, including scientific data archiving. Additionally, a new data archiving solution has been developed to demonstrate the obtainable performances and possible bottlenecks of scientific data archiving in Fast Plant System Control. The presented system implements a fault tolerant architecture over a GEthernet network where FPSC data are reliably archived on remote, while remaining accessible to be redistributed, within the duration of a pulse. The storing service is supported by a clustering solution to guaranty scalability, so that FPSC management and configuration may be simplified, and a unique view of all archived data provided. All the involved components have been integrated under EPICS [2] (Experimental Physics and Industrial Control System), implementing in each case the necessary extensions, state machines and configuration process variables. The prototyped solution is based on the NetCDF-4 [3] and [4] (Network Common Data Format) file format in order to incorporate important features, such as scientific data models support, huge size files management, platform independent codification, or single-writer/multiple-readers concurrency. In this contribution, a complete description of the above mentioned solution is presented, together with the most relevant results of the tests performed, while focusing in the benefits and limitations of the applied technologies.

ITER Fast Plant System Controller Prototype Based on Commercial PXI Platform

The ITER CODAC design identifies slow and fast plant system controllers (PSC). The gast OSCs are based on embedded technologies, permit sampling rates greater than 1 KHz, meet stringent real-time requirements, and will be devoted to data acquisition tasks and control purposes. CIEMAT and UPM have implemented a prototype of a fast PSC based on commercial off-the-shelf (COTS) technologies with PXI hardware and software based on EPICS

Abstract Interpretation-based verification/certification in the ciaoPP system

CiaoPP is the abstract interpretation-based preprocessor of the Ciao multi-paradigm (Constraint) Logic Programming system. It uses modular, incremental abstract interpretation as a fundamental tool to obtain information about programs. In CiaoPP, the semantic approximations thus produced have been applied to perform high- and low-level optimizations during program compilation, including transformations such as múltiple abstract specialization, parallelization, partial evaluation, resource usage control, and program verification. More recently, novel and promising applications of such semantic approximations are being applied in the more general context of program development such as program verification. In this work, we describe our extensión of the system to incorpórate Abstraction-Carrying Code (ACC), a novel approach to mobile code safety. ACC follows the standard strategy of associating safety certificates to programs, originally proposed in Proof Carrying- Code. A distinguishing feature of ACC is that we use an abstraction (or abstract model) of the program computed by standard static analyzers as a certifícate. The validity of the abstraction on the consumer side is checked in a single-pass by a very efficient and specialized abstractinterpreter. We have implemented and benchmarked ACC within CiaoPP. The experimental results show that the checking phase is indeed faster than the proof generation phase, and that the sizes of certificates are reasonable. Moreover, the preprocessor is based on compile-time (and run-time) tools for the certification of CLP programs with resource consumption assurances.

Interval-based resource usage verification: Formalization and prototype

In an increasing number of applications (e.g., in embedded, real-time, or mobile systems) it is important or even essential to ensure conformance with respect to a specification expressing resource usages, such as execution time, memory, energy, or user-defined resources. In previous work we have presented a novel framework for data size-aware, static resource usage verification. Specifications can include both lower and upper bound resource usage functions. In order to statically check such specifications, both upper- and lower-bound resource usage functions (on input data sizes) approximating the actual resource usage of the program which are automatically inferred and compared against the specification. The outcome of the static checking of assertions can express intervals for the input data sizes such that a given specification can be proved for some intervals but disproved for others. After an overview of the approach in this paper we provide a number of novel contributions: we present a full formalization, and we report on and provide results from an implementation within the Ciao/CiaoPP framework (which provides a general, unified platform for static and run-time verification, as well as unit testing). We also generalize the checking of assertions to allow preconditions expressing intervals within which the input data size of a program is supposed to lie (i.e., intervals for which each assertion is applicable), and we extend the class of resource usage functions that can be checked.

VOTESCRIPT: Telematic voting system designed to enable final count verification

In this paper we present a global description of a telematic voting system based on advanced cryptography and on the use of smart cards (VOTESCRIPT system) whose most outstanding characteristic is the ability to verify that the tally carried out by the system is correct, meaning that the results published by the system correspond with votes cast. The VOTESCRIPT system provides an individual verification mechanism allowing each Voter to confirm whether his vote has been correctly counted. The innovation with respect to other solutions lies in the fact that the verification process is private so that Voters have no way of proving what they voted in the presence of a non-authorized third party. Vote buying and selling or any other kind of extortion are prevented. The existence of the Intervention Systems allows the whole electoral process to be controlled by groups of citizens or authorized candidatures. In addition to this the system can simply make an audit not only of the final results, but also of the whole process. Global verification provides the Scrutineers with robust cryptographic evidence which enables unequivocal proof if the system has operated in a fraudulent way.

Design evaluation of a prototype user interface to support a guideline-based decision support system in gestational diabetes

Gestational Diabetes (GD) has increased over the last 20 years, affecting up to 15% of pregnant women worldwide. The complications associated can be reduced with the appropriate glycemic control during the pregnancy.

Low-Cost Radar-Based Target Identification Prototype using an Expert System

Smart and green cities are hot topics in current research because people are becoming more conscious about their impact on the environment and the sustainability of their cities as the population increases. Many researchers are searching for mechanisms that can reduce power consumption and pollution in the city environment. This paper addresses the issue of public lighting and how it can be improved in order to achieve a more energy efficient city. This work is focused on making the process of turning the streetlights on and off more intelligent so that they consume less power and cause less light pollution. The proposed solution is comprised of a radar device and an expert system implemented on a low-cost platform based on a DSP. By analyzing the radar echo in both the frequency and time domains, the system is able to detect and identify objects moving in front of it. This information is used to decide whether or not the streetlight should be turned on. Experimental results show that the proposed system can provide hit rates over 80%, promising a good performance. In addition, the proposed solution could be useful in kind of other applications such as intelligent security and surveillance systems and home automation.