The aim of this study is to present electrooculogram signals that can be used for human computer interface efficiently. Establishing an efficient alternative channel for communication without overt speech and hand movements is important to increase the quality of life for patients suffering from Amyotrophic Lateral Sclerosis or other illnesses that prevent correct limb and facial muscular responses. In this paper, we introduce the gaze estimation system of electrooculogram signals. Using this system, the electrooculogram signals can be recorded when the patients focused on each direct. All these recorded signals could be analyzed using math-method and the mathematical model will be set up. Gaze estimation can be recognized using electrooculogram signals follow these models.

This paper presents a graph-based approach to designing arithmetic circuits over Galois fields (GFs) using normal basis representations. The proposed method is based on a graph-based circuit description called Galois-field Arithmetic Circuit Graph (GF-ACG). First, we extend GF-ACG representation to describe GFs defined by normal basis in addition to polynomial basis. We then apply the extended design method to Massey-Omura parallel multipliers which are well known as typical multipliers based on normal basis. We present the formal description of the multipliers in a hierarchical manner and show that the verification time can be greatly reduced in comparison with those of the conventional techniques. In addition, we design GF exponentiation circuits consisting of the Massey-Omura parallel multipliers and an inversion circuit over composite field GF(((22)2)2) in order to demonstrate the advantages of normal-basis circuits over polynomial-basis ones.

This paper addresses the problems of fingerprint identification and verification when a query fingerprint is taken under conditions that differ from those under which the fingerprint of the same person stored in a database was constructed. This occurs when using a different fingerprint scanner with a different pressure, resulting in a fingerprint impression that is smeared and distorted in accordance with a geometric transformation (e.g., affine or even non-linear). Minutiae points on a query fingerprint are matched and aligned to those on one of the fingerprints in the database, using a set of absolute invariants constructed from the shape and/or size of minutiae triangles depending on the assumed map. Once the best candidate match is declared and the corresponding minutiae points are flagged, the query fingerprint image is warped against the candidate fingerprint image in accordance with the estimated warping map. An identification/verification cost function using a combination of distance map and global directional filterbank (DFB) features is then utilized to verify and identify a query fingerprint against candidate fingerprint(s). Performance of the algorithm yields an area of 0.99967 (perfect classification is a value of 1) under the receiver operating characteristic (ROC) curve based on a database consisting of a total of 1680 fingerprint images captured from 240 fingers. The average probability of error was found to be 0.713%. Our algorithm also yields the smallest false non-match rate (FNMR) for a comparable false match rate (FMR) when compared to the well-known technique of DFB features and triangulation-based matching integrated with modeling non-linear deformation. This work represents an advance in resolving the fingerprint identification problem beyond the state-of-the-art approaches in both performance and robustness.

In this paper we report on experiences gained and lessons learned by the use of the Timed OTS/CafeOBJ method in the formal verification of TESLA source authentication protocol. These experiences can be a useful guide for the users of the OTS/CafeOBJ, especially when dealing with such complex systems and protocols.

There have been many researches about construction and application of ontology in reality, notably the usage of ontology to support requirements engineering. The effect of ontology-based requirements engineering depends on quality of ontology. With the increasing size of ontology, it is difficult to verify the correctness of information stored in ontology. This paper will propose a method of using rules for verification the correctness of requirements ontology. We provide a rule description language to specify properties that requirements ontology should satisfy. Then, by checking whether the rules are consistent with requirements ontology, we verify the correctness of the ontology. We have developed a verification tool to support the method and evaluated the tool through experiments.

This paper introduces an ontology-based method for checking requirements specification. Requirements ontology is a knowledge structure that contains functional requirements (FR), attributes of FR and relations among FR. Requirements specification is compared with functional nodes in the requirements ontology, then rules are used to find errors in requirements. On the basis of the results, requirements team can ask questions to customers and correctly and efficiently revise requirements. To support this method, an ontology-based checking tool for verification of requirements has been developed. Finally, the requirements checking method is evaluated through an experiment.

This paper presents a method for automatic rectification of design bugs in processors. Given a golden sequential instruction-set architecture model of a processor and its erroneous detailed cycle-accurate model at the micro-architecture level, we perform symbolic simulation and property checking combined with concrete simulation iteratively to detect the buggy location and its corresponding fix. We have used the truth-table model of the function that is required for correction, which is a very general model. Moreover, we do not represent the truth-table explicitly in the design. We use, instead, only the required minterms, which are obtained from the output of our backend formal engine. This way, we avoid adding any new variable for representing the truth-table. Therefore, our correction model is scalable to the number of inputs of the truth-table that could grow exponentially. We have shown the effectiveness of our method on a complex out-of-order superscalar processor supporting atomic execution of instructions. Our method reduces the model size for correction by 6.0x and total correction time by 12.6x, on average, compared to our previous work.

MapReduce is commonly used as a parallel massive data processing model. When deploying it as a service over the open systems, the computational integrity of the participants is becoming an important issue due to the untrustworthy workers. Current duplication-based solutions can effectively solve non-collusive attacks, yet most of them require a centralized worker to re-compute additional sampled tasks to defend collusive attacks, which makes the worker a bottleneck. In this paper, we try to explore a trusted worker scheduling framework, named VAWS, to detect collusive attackers and assure the integrity of data processing without extra re-computation. Based on the historical results of verification, we construct an Integrity Attestation Graph (IAG) in VAWS to identify malicious mappers and remove them from the framework. To further improve the efficiency of identification, a verification-couple selection method with the IAG guidance is introduced to detect the potential accomplices of the confirmed malicious worker. We have proven the effectiveness of our proposed method on the improvement of system performance in theoretical analysis. Intensive experiments show the accuracy of VAWS is over 97% and the overhead of computation is closed to the ideal value of 2 with the increasing of the number of map tasks in our scheme.

Superconducting Single-Flux-Quantum (SFQ) devices have been paid much attention as alternative devices for digital circuits, because of their high switching speed and low power consumption. For large-scale circuit design, the role of computer-aided design environment is significant. As the characteristics of the SFQ devices are different from conventional devices, a new design environment is required. In this paper, we propose a new timing-aware circuit description method which can be used for SFQ circuit design. Based on the description and the dedicated algorithms we have been developing for SFQ logic circuit design, we propose an integrated design flow for SFQ logic circuits. We have designed a circuit using our developed design tools along with the design flow and demonstrated the correct operation.

Many discrete functions are often compactly represented by Decision Diagrams (DD). The main problem in the construction of decision diagrams is the space and time requirements. While constructing a decision diagram the memory requirement may grow exponentially with the function. Also, large numbers of temporary nodes are created while constructing the decision diagram for a function. Here the problem of reducing the number of temporary nodes is addressed with respect to the PLA specification format of a function, where the function is represented using a set of cubes. Usually a DD is constructed by recursively processing the input cubes in the PLA specification. The DD, representing a sub function, is specified by a single cube. This DD is merged with a master DD, which represents the entire previously processed cubes. Thus the master DD is constructed recursively, until all the cubes in the input cube set are processed. In this paper, an efficient method is proposed, which reorders and also partitions the cube set into unequal number of cubes per subset, in such a way that, the number of temporary nodes created and the number of logical operations done, during the merging of cubes with the master DD are reduced. This results in the reduction of space and time required for the construction of DDs to a remarkable extent.

Computation integrity is difficult to verify when mass data processing is outsourced. Current integrity protection mechanisms and policies verify results generated by participating nodes within a computing environment of service providers (SP), which cannot prevent the subjective cheating of SPs. This paper provides an analysis and modeling of computation integrity for mass data processing services. A third-party sampling-result verification method, named TS-TRV, is proposed to prevent lazy cheating by SPs. TS-TRV is a general solution of verification on the intermediate results of common MapReduce jobs, and it utilizes the powerful computing capability of SPs to support verification computing, thus lessening the computing and transmission burdens of the verifier. Theoretical analysis indicates that TS-TRV is effective on detecting the incorrect results with no false positivity and almost no false negativity, while ensuring the authenticity of sampling. Intensive experiments show that the cheating detection rate of TS-TRV achieves over 99% with only a few samples needed, the computation overhead is mainly on the SP, while the network transmission overhead of TS-TRV is only O(log N).

Verifiable random functions (VRF), proposed in 1999, and selectively convertible undeniable signature (SCUS) schemes, proposed in 1990, are apparently thought as independent primitives in the literature. In this paper, we show that they are tightly related in the following sense: VRF is exactly SCUS; and the reverse also holds true under a condition. This directly yields several deterministic SCUS schemes based on existing VRF constructions. In addition, we create a new probabilistic SCUS scheme, which is very compact. We build efficient confirmation and disavowal protocols for the proposed SCUS schemes, based on what we call zero-knowledge protocols for generalized DDH and non-DDH. These zero-knowledge protocols are built either sequential, concurrent, or universally composable.

Face verification is the task of determining whether two given face images represent the same person or not. It is a very challenging task, as the face images, captured in the uncontrolled environments, may have large variations in illumination, expression, pose, background, etc. The crucial problem is how to compute the similarity of two face images. Metric learning has provided a viable solution to this problem. Until now, many metric learning algorithms have been proposed, but they are usually limited to learning a linear transformation. In this paper, we propose a nonlinear metric learning method, which learns an explicit mapping from the original space to an optimal subspace using deep Independent Subspace Analysis (ISA) network. Compared to the linear or kernel based metric learning methods, the proposed deep ISA network is a deep and local learning architecture, and therefore exhibits more powerful ability to learn the nature of highly variable dataset. We evaluate our method on the Labeled Faces in the Wild dataset, and results show superior performance over some state-of-the-art methods.

In the Cloud computing era, users could have their data outsourced to cloud service provider (CSP) to enjoy on-demand high quality service. On the behalf of the user, a third party auditor (TPA) which could verify the real data possession on CSP is critically important. The central challenge is to build efficient and provably secure data verification scheme while ensuring that no users' privacy is leaked to any unauthorized party, including TPA. In this paper, we propose the first identity-based public verification scheme, based on the identity-based aggregate signature (IBAS). In particular, by minimizing information that verification messages carry and TPA obtains or stores, we could simplify key management and greatly reduce the overheads of communication and computation. Unlike the existing works based on certificates, in our scheme, only a private key generator (PKG) has a traditional public key while the user just keeps its identity without binding with certificate. Meanwhile, we utilize privacy-preserving technology to keep users' private data off TPA. We also extend our scheme with the support of batch verification task to enable TPA to perform public audits among different users simultaneously. Our scheme is provably secure in the random oracle model under the hardness of computational Diffie-Hellman assumption over pairing-friendly groups and Discrete Logarithm assumption.

As an extension of H.264/AVC, Scalable Video Coding (SVC) provides the ability to adapt to heterogeneous networks and user-end requirements, which offers great scalability in multi-point applications such as videoconferencing. However, transcoding between SVC and AVC becomes necessary due to the existence of legacy AVC-based systems. The straightforward full re-encoding method requires great computational cost, and the fast SVC-to-AVC spatial transcoding techniques have not been thoroughly investigated yet. This paper proposes a low-complexity hybrid-domain SVC-to-AVC spatial transcoder with drift compensation, which provides even better coding efficiency than the full re-encoding method. The macroblocks (MBs) of input SVC bitstream are divided into two types, and each type is suitable for pixel- or transform-domain processing respectively. In the pixel-domain transcoding, a fast re-encoding method is proposed based on mode mapping and motion vector (MV) refinement. In the transform-domain transcoding, the quantized transform coefficients together with other motion data are reused directly to avoid re-quantization loss. The drift problem caused by proposed transcoder is solved by compensation techniques for I frame and P frame respectively. Simulation results show that proposed transcoder achieves averagely 96.4% time reduction compared with the full re-encoding method, and outperforms the reference methods in coding efficiency.

We propose a composite DCT basis line test signal to evaluate the video quality of a DTV encoder. The proposed composite test signal contains a frame index, a calibration square wave, and 7-field basis signals. The results show that the proposed method may be useful for an in-service video quality verifier, using an ordinary oscilloscope instead of special equipment.

At Eurocrypt'03, Boneh, Gentry, Lynn and Shacham proposed a pairing based verifiably encrypted signature scheme (the BGLS-VES scheme). In 2004, Hess mounted an efficient rogue-key attack on the BGLS-VES scheme in the plain public-key model. In this letter, we show that the BGLS-VES scheme is not secure in the proof of possession (POP) model.

In 2004, Menezes and Smart left an open problem that is whether there exists a realistic scenario where message and key substitution (MKS) attacks can have damaging consequences. In this letter, we show that MKS attacks can have damaging consequences in practice, by pointing out that a verifiably encrypted signature (VES) scheme is not opaque if MKS attacks are possible.

Developing a complex network accelerator like an IPsec processor is a great challenge. To this end, we propose a Network Virtual Platform ( NetVP ) that consists of one or more virtual host (vHOST) modules and virtual local area network (vLAN) modules to support electronic system level (ESL) top-down design flow as well as provide the on-line verification throughout the entire development process. The on-line verification capability of NetVP enables the designed target to communicate with a real network for system validation. For ESL top-down design flow, we also propose untimed and timed interfaces to support hardware/software co-simulation. In addition, the NetVP can be used in conjunction with any ESL development platform through the untimed/timed interface. System development that uses this NetVP is efficient and flexible since it allows the designer to explore design spaces such as the network bandwidth and system architecture easily. The NetVP can also be applied to the development of other kinds of network accelerators.

Initial cell search in wideband code-division multiple-access (W-CDMA) systems is a challenging process. On the one hand, channel impairments such as multipath fading, Doppler shift, and noise create frequency and time offsets in the received signal. On the other hand, the residual synchronization error of the crystal oscillator at the mobile station also causes time and frequency offsets. Such offsets can affect the ability of a mobile station to perform cell search. Previous work concentrated on cell synchronization algorithms that considered multipath channels and frequency offsets, but ignored clock and timing offsets due to device tolerances. This work discusses a robust initial cell search algorithm, and quantifies its performance in the presence of frequency and time offsets due to two co-existing problems: channel impairments and clock drift at the receiver. Another desired performance enhancement is the reduction of power consumption of the receiver, which is mainly due to the computational complexity of the algorithms. This power reduction can be achieved by reducing the computational complexity by a divide and conquer strategy during the synchronization process.