Homomorphic encryption allows computation over encrypted data, and can be used for delegating computation: data providers encrypt their data and send them to an aggregator, who can then perform computation over the encrypted data on behalf of a client, without the underlying data being exposed to the aggregator. However, since the aggregator is merely a third party, it may be malicious, and in particular, may submit an incorrect aggregation result to the receiver. Ohara et al. (APKC2014) studied secure aggregation of time-series data while enabling the correctness of aggregation to be verified. However, they only provided a concrete construction in the smart metering system and only gave an intuitive argument of security. In this paper, we define verifiable homomorphic encryption (VHE) which generalizes their scheme, and introduce formal security definitions. Further, we formally prove that Ohara et al.'s VHE scheme satisfies our proposed security definitions.

This study evaluates the effects of some non-learning blind bandwidth extension (BWE) methods on state-of-the-art automatic speaker verification (ASV) systems. Recently, a non-linear bandwidth extension (N-BWE) method has been proposed as a blind, non-learning, and light-weight BWE approach. Other non-learning BWEs have also been developed in recent years. For ASV evaluations, most data available to train ASV systems is narrowband (NB) telephone speech. Meanwhile, wideband (WB) data have been used to train the state-of-the-art ASV systems, such as i-vector, d-vector, and x-vector. This can cause sampling rate mismatches when all datasets are used. In this paper, we investigate the influence of sampling rate mismatches in the x-vector-based ASV systems and how non-learning BWE methods perform against them. The results showed that the N-BWE method improved the equal error rate (EER) on ASV systems based on the x-vector when the mismatches were present. We researched the relationship between objective measurements and EERs. Consequently, the N-BWE method produced the lowest EERs on both ASV systems and obtained the lower RMS-LSD value and the higher STOI score.

Since software becomes more complex during its life cycle, the verification cost becomes higher, especially for such methods which are using model checking in general and assume-guarantee reasoning in specific. To address the problem of reducing the assume-guarantee verification cost, this paper presents a method to generate locally minimum and strongest assumptions for verification of component-based software. For this purpose, we integrate a variant of membership queries answering technique to an algorithm which considers candidate assumptions that are smaller and stronger first, larger and weaker later. Because the algorithm stops as soon as it reaches a conclusive result, the generated assumptions are the locally minimum and strongest ones. The correctness proof of the proposed algorithm is also included in the paper. An implemented tool, test data, and experimental results are presented and discussed.

Java is one of important program language today. In Java, in order to build sound software, we have to carefully implement two fundamental methods hashCode and equals. This requirement, however, is not easy to follow in real software development. Some existing studies for ensuring the correctness of these two methods rely on static analysis, which are limited to loop-free programs. This paper proposes a new solution to this important problem, using software analysis workbench (SAW), an open source tool. The efficiency is evaluated through experiments. We also provide a useful situation where cost of regression testing is reduced when program refactoring is conducted.

LINE is currently the most popular messaging service in Japan. Communications using LINE are protected by the original encryption scheme, called LINE Encryption, and specifications of the client-to-server transport encryption protocol and the client-to-client message end-to-end encryption protocol are published by the Technical Whitepaper. Though a spoofing attack (i.e., a malicious client makes another client misunderstand the identity of the peer) and a reply attack (i.e., a message in a session is sent again in another session by a man-in-the-middle adversary, and the receiver accepts these messages) to the end-to-end protocol have been shown, no formal security analysis of these protocols is known. In this paper, we show a formal verification result of secrecy of application data and authenticity for protocols of LINE Encryption (Version 1.0) by using the automated security verification tool ProVerif. Especially, since it is claimed that the transport protocol satisfies forward secrecy (i.e., even if the static private key is leaked, security of application data is guaranteed), we verify forward secrecy for client's data and for server's data of the transport protocol, and we find an attack to break secrecy of client's application data. Moreover, we find the spoofing attack and the reply attack, which are reported in previous papers.

This paper proposes a speaker-phonetic i-vector modeling method for text-dependent speaker verification with random digit strings, in which enrollment and test utterances are not of the same phrase. The core of the proposed method is making use of digit alignment information in i-vector framework. By utilizing force alignment information, verification scores of the testing trials can be computed in the fixed-phrase situation, in which the compared speech segments between the enrollment and test utterances are of the same phonetic content. Specifically, utterances are segmented into digits, then a unique phonetically-constrained i-vector extractor is applied to obtain speaker and channel variability representation for every digit segment. Probabilistic linear discriminant analysis (PLDA) and s-norm are subsequently used for channel compensation and score normalization respectively. The final score is obtained by combing the digit scores, which are computed by scoring individual digit segments of the test utterance against the corresponding ones of the enrollment. Experimental results on the Part 3 of Robust Speaker Recognition (RSR2015) database demonstrate that the proposed approach significantly outperforms GMM-UBM by 52.3% and 53.5% relative in equal error rate (EER) for male and female respectively.

In the model of no-dictionary searchable symmetric encryption (SSE) schemes, the client does not need to keep the list of keywords W. In this paper, we first show a generic method to transform any passively secure SSE scheme to a no-dictionary SSE scheme such that the client can verify search results even if w ∉ W. In particular, it takes only O(1) time for the server to prove that w ∉ W. We next present a no-dictionary SSE scheme such that the client can hide even the search pattern from the server.

Defects in spacecraft software may result in loss of life and serious economic damage. To avoid such consequences, the software development process incorporates code review activity. A code review conducted by a third-party organization independently of a software development team can effectively identify defects in software. However, such review activity is difficult for third-party reviewers, because they need to understand the entire structure of the code within a limited time and without prior knowledge. In this study, we propose a tool to visualize inter-module dataflow for source code of spacecraft software systems. To evaluate the method, an autonomous rover control program was reviewed using this visualization. While the tool does not decreases the time required for a code review, the reviewers considered the visualization to be effective for reviewing code.

In multiprocessors, memory models are introduced to describe the executions of programs among processors. Relaxed memory models, which relax the order of executions, are used in the most of the modern processors, such as ARM and POWER. Due to a relaxed memory model could change the program semantics, the executions of the programs might not be the same as our expectation that should preserve the program correctness. In addition to relaxed memory models, the way to execute an instruction is described by an instruction semantics, which varies among processor architectures. Dealing with instruction semantics among a variety of assembly programs is a challenge for program verification. Thus, this paper proposes a way to verify a variety of assembly programs that are executed under a relaxed memory model. The variety of assembly programs can be abstracted as the way to execute the programs by introducing an operation structure. Besides, there are existing frameworks for modeling relaxed memory models, which can realize program executions to be verified with a program property. Our work adopts an SMT solver to automatically reveal the program executions under a memory model and verify whether the executions violate the program property or not. If there is any execution from the solver, the program correctness is not preserved under the relaxed memory model. To verify programs, an experimental tool was developed to encode the given programs for a memory model into a first-order formula that violates the program correctness. The tool adopts a modeling framework to encode the programs into a formula for the SMT solver. The solver then automatically finds a valuation that satisfies the formula. In our experiments, two encoding methods were implemented based on two modeling frameworks. The valuations resulted by the solver can be considered as the bugs occurring in the original programs.

Intensity modulated radiation therapy (IMRT), which irradiates doses to a target organ, calculates the irradiation dose using the radiation treatment planning system (RTPS). The irradiation quality is ensured by verifying that the dose distribution planned by RTPS is the same as the data measured by two-dimensional (2D) detectors. Since an actual three-dimensional (3D) distribution of irradiated dose spreads complicatedly, it is different from that of RTPS. Therefore, it is preferable to evaluate by using not only RTPS, but also actual irradiation dose distribution. In this paper, in order to perform a dose-volume histogram (DVH) evaluation of the irradiation dose distribution, we propose a method of correcting the dose distribution of RTPS by using sparsely measured radial data from 2D dose detectors. And we perform a DVH evaluation of irradiation dose distribution and we show that the proposed method contributes to high-precision DVH evaluation. The experimental results show that the estimates are in good agreement with the measured data from the 2D detectors and that the peak signal to noise ratio and the structural similarity indexes of the estimates are more accurate than those of RTPS. Therefore, we present the possibility of an evaluation of the actual irradiation dose distribution using measured data in a limited observation direction.

In order to verify the correctness of functional requirements, we have been developing a verification method of the correctness of functional requirements specification using the Requirements Frame model. In this paper, we propose a verification method of non-functional requirements specification in terms of time-response requirements written with a natural language. We established a verification method by extending the Requirements Frame model. We have also developed a prototype system based on the method using Java. The extended Requirements Frame model and the verification method will be illustrated with examples.

Simulation-based verification of hardware designs, in particular, register-transfer-level (RTL) designs, has been widely used, and has been one of the major bottlenecks in design processes. One of the approaches is coverage-driven verification, of its target is improvement of some metric called coverage. In a prior work of ours, we have proposed a coverage-driven verification using both randomly generated simulation patterns and patterns generated by a SAT (satisfiability) solver, and have shown its effectiveness. In this paper, we extend this approach with an SMT (satisfiability modulo theory) solver, which can handle arithmetic relations among integer, floating-point or bit-vector variables. Experimental results show that the more arithmetic modules are included, the more an SMT-based method gets superior to the method using only a SAT solver.

With the popularity of cloud computing services, outsourcing computation has entered a period of rapid development. Modular exponentiation is one of the most expensive operations in public key cryptographic systems, but the current outsourcing algorithms for modular exponentiations (MExps) with single server are inefficient or have small checkability. In this paper, we propose an efficient and fully verifiable algorithm for outsourcing multiple MExps with single untrusted server where the errors can be detected by an outsourcer with a probability of 1. The theory analysis and experimental evaluations also show that the proposed algorithm is the most efficient one compared with the previous work. Finally, we present the outsourcing schemes of digital signature algorithm (DSA) and attribute based encryption (ABE) as two applications of the proposed algorithm.

In data stream analysis, detecting the concept drift accurately is important to maintain the classification performance. Most drift detection methods assume that the class labels become available immediately after a data sample arrives. However, it is unrealistic to attempt to acquire all of the labels when processing the data streams, as labeling costs are high and much time is needed. In this paper, we propose a concept drift detection method under the assumption that there is limited access or no access to class labels. The proposed method detects concept drift on unlabeled data streams based on the class label information which is predicted by a classifier or a virtual classifier. Experimental results on synthetic and real streaming data show that the proposed method is competent to detect the concept drift on unlabeled data stream.

An automotive control system is a typical safety-critical embedded software, which requires extensive verification and validation (V&V) activities. This article introduces a toolset for automated V&V of automotive control system, including a test generator for automotive operating systems, a task simulator for validating task design of control software, and an API-call constraint checker to check emergent properties when composing control software with its underlying operating system. To the best of our knowledge, it is the first integrated toolset that supports V&V activities for both control software and operating systems in the same framework.

Verification of logic designs has been a long-standing bottleneck in the process of hardware design, where its automation and improvement of efficiency has demanding needs. Mainly simulation-based verification has been used for this purpose, and recently, coverage-driven verification has been widely used, of which target is improvement of some metric called coverage. Our target is the metric called toggle coverage. To find input patterns which cause some toggles on each signal, a SAT solver could be used, but this is computationally costly. In this paper, we study the effect of combination of random simulation and usage of a SAT solver. In particular, we use a SAT solver which can find multiple “diverse” solutions. With this solver, we can avoid generating similar patterns, which are unlikely to improve coverage. The experimental results show that, a small number of calls of a SAT solver can improve entire toggle coverage effectively, compared with simple random simulation.

The rapid prototyping of a mixed-signal system-on-chip (SoC) has been enabled by reusing predesigned intellectual properties (IPs) and by integrating newly designed IP into the top design of SoC. The IPs have been designed on various hardware description levels, which leads to challenges in simulations that evaluate the prototyping. One traditional solution is to convert these heterogeneous IP models into equivalent models, that are described in a single description language. This conversion approach often requires manual rewriting of existing IPs, and this results in description loss during the model projection due to the absence of automatic conversion tools. The other solutions are co-simulation/emulation approaches that are based on the coupling of multiple simulators/emulators through connection modules. The conventional methods do not have formal theoretical backgrounds and an explicit interface for integrating the simulator into their solutions. In this paper, we propose a general co-simulation approach based on the high-level architecture (HLA) and a newly-defined programming language interface for interoperation (PLI-I) between heterogeneous IPs as a formal simulator interface. Based on the proposed PLI-I and HLA, we introduce formal procedures of integration and interoperation. To reduce integration costs, we split these procedures into two parts: a reusable common library and an additional model-dependent signal-to-event (SE) converter to handle differently abstracted in/out signals between the coupled IPs. During the interoperation, to resolve the different time-advance mechanisms and increase computation concurrency between digital and analog simulators, the proposed co-simulation approach performs an advanced HLA-based synchronization using the pre-simulation concepts. The case study shows the validation of interoperation behaviors between the heterogeneous IPs in mixed-signal SoC design, the reduced design effort in integrating, and the synchronization speedup using the proposed approach.

In accordance with Moore's law, recent design issues include shortening of time-to-market and detection of delay faults. Several studies with respect to formal techniques have examined the first issue. Using the equivalence checking, it is possible to identify whether large circuits are equivalent or not in a practical time frame. With respect to the latter issue, it is difficult to achieve 100% fault efficiency even for transition faults in full scan designs. This study involved proposing a redundant transition fault identification method using equivalence checking. The main concept of the proposed algorithm involved combining the following two known techniques, 1. modeling of a transition fault as a stuck-at fault with temporal expansion and 2. detection of a stuck-at fault by using equivalence checking tools. The experimental results indicated that the proposed redundant identification method using a formal approach achieved 100% fault efficiency for all benchmark circuits in a practical time even if a commercial ATPG tool was unable to achieve 100% fault efficiency for several circuits.

This paper proposes a formal approach of verifying ubiquitous computing application scenarios. Ubiquitous computing application scenarios assume that there are a lot of devices and physical things with computation and communication capabilities, which are called smart objects, and these are interacted with each other. Each of these interactions among smart objects is called “federation”, and these federations form a ubiquitous computing application scenario. Previously, Yuzuru Tanaka proposed “a proximity-based federation model among smart objects”, which is intended for liberating ubiquitous computing from stereotyped application scenarios. However, there are still challenges to establish the verification method of this model. This paper proposes a verification method of this model through model checking. Model checking is one of the most popular formal verification approach and it is often used in various fields of industry. Model checking is conducted using a Kripke structure which is a formal state transition model. We introduce a context catalytic reaction network (CCRN) to handle this federation model as a formal state transition model. We also give an algorithm to transform a CCRN into a Kripke structure and we conduct a case study of ubiquitous computing scenario verification, using this algorithm and the model checking. Finally, we discuss the advantages of our formal approach by showing the difficulties of our target problem experimentally.

Narrow swipe sensor has been widely used in embedded systems such as smart-phone. However, the size of captured image is much smaller than that obtained by the traditional area sensor. Therefore, the limited template coverage is the performance bottleneck of such kind of systems. Aiming to increase the geometry coverage of templates, a novel fingerprint template feature synthesis scheme is proposed in the present study. This method could synthesis multiple input fingerprints into a wider template by clustering the minutiae descriptors. The proposed method consists of two modules. Firstly, a user behavior-based Registration Pattern Inspection (RPI) algorithm is proposed to select the qualified candidates. Secondly, an iterative clustering algorithm Modified Fuzzy C-Means (MFCM) is proposed to process the large amount of minutiae descriptors and then generate the final template. Experiments conducted over swipe fingerprint database validate that this innovative method gives rise to significant improvements in reducing FRR (False Reject Rate) and EER (Equal Error Rate).