BGP dictates routing between autonomous systems with rich policy mechanisms in today's Internet. Operators translate high-level policy principles into low-level configurations of multiple routers without a comprehensive understanding of the actual effect on the network behaviors, making the routing management and operation an error-prone and time-consuming procedure. A fundamental question to answer is: how to verify the intended routing principles against the actual routing effects of an ISP? In this paper, we develop a methodology RPIM (Routing Policy Inference Model) towards this end. RPIM extracts from the routing tables various policy patterns, which represent certain high-level policy intentions of network operators, and then maps the patterns into specific design primitives that the ISP employs. To the best of our knowledge, we are the first to infer routing policies in ISP networks comprehensively from the aspects of business relationship, traffic engineering, scalability and security. We apply RPIM to 11 ASes selected from RIPE NCC RIS project, and query IRR database to validate our approach. Vast majority of inferred policies are confirmed by the policy registries, and RPIM achieves 96.23% accuracy excluding validation difficulties caused by incompleteness of the IRR database.

This paper presents a 7 GHz differential current-reused voltage-controlled oscillator (CR-VCO) with low power consumption and low phase noise using 0.18-µm CMOS technology. The output power of this CR-VCO is enhanced by utilizing a trifilar-transformer-feedback technique. The lower phase noise is achieved by the more symmetric voltage swings resulting from the improved balance of switching current. At a 1.5-V DC supply voltage, the power dissipation is only 3.4 mW. The total tuning range is 1.4 GHz (17.9%) as the tuning voltage ranges from 0 V to 1.8 V. The optimum phase noise is around -117.3 dBc/Hz at a frequency offset of 1 MHz from the center frequency of 7.07 GHz. The corresponding output power is around -6.8 dBm. For the proposed CR-VCO, the calculated figures-of-merit, FOM and FOMT , are -188.9 and -193.9 dBc/Hz, respectively.

This paper presents a non-interactive verifiable secret sharing scheme (VSS) tolerating a dishonest majority based on data pre-distributed by a trusted authority. As an application of this VSS scheme we present very efficient unconditionally secure protocols for performing multiplication of shares based on pre-distributed data which generalize two-party computations based on linear pre-distributed bit commitments. The main results of this paper are a non-interactive VSS, a simplified multiplication protocol for shared values based on pre-distributed random products, and non-interactive zero knowledge proofs for arbitrary polynomial relations. The security of the schemes is proved using the UC framework.

Bounded model checking is a widely used formal technique in both hardware and software verification. However, it cannot be applied if the bounds (number of time frames to be analyzed) become large, and deep bugs which are observed only through very long counter-examples cannot be detected. This paper presents a method concatenating multiple bounded model checking results efficiently with symbolic simulation. A bounded model checking with a large bound is recursively decomposed into multiple ones with smaller bounds, and symbolic simulation on each counterexample supports smooth connections to the others. A strong heuristic for the proposed method that targets deep bugs is also presented, and can be applied together with other efficient bounded model checking methods since it does not touch the basic bounded model checking algorithm.

This paper discusses speaker verification (SV) using Gaussian mixture models (GMMs), where only utterances of enrolled speakers are required. Such an SV system can be realized using artificially generated cohorts instead of real cohorts from speaker databases. This paper presents a rational approach to set GMM parameters for artificial cohorts based on statistics of GMM parameters for real cohorts. Equal error rates for the proposed method are about 10% less than those for the previous method, where GMM parameters for artificial cohorts were set in an ad hoc manner.

A hash chain H for a hash function hash(·) is a sequence of hash values ⟨ xn, xn-1,..., x0 ⟩, where x0 is a secret value, xi is generated by xi = hash(xi-1) for 1 ≤ i ≤ n, and xn is a public value. Hash values of H are disclosed gradually from xn-1 to x0. The correctness of a disclosed hash value xi can be verified by checking the equation xn =? hashn-i(xi). To speed up the verification, Fischlin introduced a check-bit scheme at CT-RSA 2004. The basic idea of the check-bit scheme is to output some extra information cb, called a check-bit vector, in addition to the public value xn, which allows each verifier to perform only a fraction of the original work according to his or her own security level. We revisit the Fischlin's check-bit scheme and show that the length of the check-bit vector cb can be reduced nearly by half. The reduced length of cb is close to the theoretic lower bound.

Clock driver suffers from delay variation due to manufacturing and environmental variabilities as well as combinational cells. The delay variation causes clock skew and jitter, and varies both setup and hold timing margins. This paper presents a timing verification method that takes into consideration delay variation inside a clock network due to both manufacturing variability and dynamic power supply noise. We also discuss that setup and hold slack computation inherently involves a structural correlation problem due to common paths, and demonstrate that assigning individual random variables to upstream clock drivers provides a notable accuracy improvement in clock skew estimation with limited increase in computational cost. We applied the proposed method to industrial designs in 90 nm process. Experimental results show that dynamic delay variation reduces setup slack by over 500 ps and hold slack by 16.4 ps in test cases.

We present an alternative approach to what we call the "standard optimization", which minimizes a cost function by searching a parameter space. Instead, our approach "projects" in the joint observation space onto the manifold defined by the "consistency constraint", which demands that any minimal subset of observations produce the same result. This approach avoids many difficulties encountered in the standard optimization. As typical examples, we apply it to line fitting and multiview triangulation. The latter produces a new algorithm far more efficient than existing methods. We also discuss the optimality of our approach.

This paper presents a low-power System on Chip (SOC) architecture for the v2.0+EDR (Enhanced Data Rate) Bluetooth and its applications. Our design includes a link controller, modem, RF transceiver, Sub-Band Codec (SBC), Expanded Instruction Set Computer (ESIC) processor, and peripherals. To decrease power consumption of the proposed SOC, we reduce data transfer using a dual-port memory, including a power management unit, and a clock gated approach. We also address some of issues and benefits of reusable and unified environment on a centralized data structure and SOC verification platform. This includes flexibility in meeting the final requirements using technology-independent tools wherever possible in various processes and for projects. The other aims of this work are to minimize design efforts by avoiding the same work done twice by different people and to reuse the similar environment and platform for different projects. This chip occupies a die size of 30 mm2 in 0.18 µm CMOS, and the worst-case current of the total chip is 54 mA.

In this paper we introduce a new framework of audio processing, which is essential to achieve a trigger-free speech interface for home appliances. If the speech interface works continually in real environments, it must extract occasional voice commands and reject everything else. It is extremely important to reduce the number of false alarms because the number of irrelevant inputs is much larger than the number of voice commands even for heavy users of appliances. The framework, called Intentional Voice Command Detection, is based on voice activity detection, but enhanced by various speech/audio processing techniques such as emotion recognition. The effectiveness of the proposed framework is evaluated using a newly-collected large-scale corpus. The advantages of combining various features were tested and confirmed, and the simple LDA-based classifier demonstrated acceptable performance. The effectiveness of various methods of user adaptation is also discussed.

An assume-guarantee verification method has been recognized as a promising approach to verify component-based software by model checking. This method is not only fitted to component-based software but also has a potential to solve the state space explosion problem in model checking. The method allows us to decompose a verification target into components so that we can model check each of them separately. In this method, assumptions are seen as the environments needed for the components to satisfy a property and for the rest of the system to be satisfied. The number of states of the assumptions should be minimized because the computational cost of model checking is influenced by that number. Thus, we propose a method for generating minimal assumptions for the assume-guarantee verification of component-based software. The key idea of this method is finding the minimal assumptions in the search spaces of the candidate assumptions. The minimal assumptions generated by the proposed method can be used to recheck the whole system at much lower computational cost. We have implemented a tool for generating the minimal assumptions. Experimental results are also presented and discussed.

Bus-based system-on-a-chip (SoC) design has become the major integrated methodology for shortening SoC design time. The main challenge is how to verify on-chip bus protocols efficiently. Although traditional simulation-based bus protocol monitors can check whether bus signals obey bus protocol or not. They are still lack of an efficient bus protocols verification environment such as FPGA-level or chip-level. To overcome the shortage, we propose a rule-based synthesizable AMBA AHB on-chip bus protocol checker, which contains 73 related AHB on-chip bus protocol rules to check AHB bus signal behaviors, and two corresponding verification mechanisms: an error reference table (ERT) and a windowed trace buffer, to shorten verification time.

Layout-aware compact models proposed so far have been generally verified only for simple test patterns. However, real designs use much more complicated layout patterns. Therefore, models must be verified for such patterns to establish their practicality. This paper proposes a methodology and test patterns for exhaustively and systematically validating layout-aware compact models for general layout patterns for the first time. The methodology and test patterns are concretely shown through validation of a shallow trench isolation (STI) stress compact model proposed in [1]. First, the model parameters for a 55-nm CMOS technology are extracted, and then the model is verified and established to be accurate for the basic patterns used for parameter extraction. Next, fundamental ideas of model operation for general layout patterns are verified using various verification patterns. These tests revealed that the model is relatively weak in some cases not included in the basic patterns. Finally, the errors for these cases are eliminated by enhancing the algorithm. Consequently, the model is confirmed to have high generality. This methodology will be effective for validating other layout-aware compact models for general layout patterns.

Cancelable approaches for biometric person authentication have been studied to protect enrolled biometric data, and several algorithms have been proposed. One drawback of cancelable approaches is that the performance is inferior to that of non-cancelable approaches. In this paper, we propose a scheme to improve the performance of a cancelable approach for online signature verification. Our scheme generates two cancelable dataset from one raw dataset and uses them for verification. Preliminary experiments were performed using a distance-based online signature verification algorithm. The experimental results show that our proposed scheme is promising.

A new estimation algorithm of clock drift in symbol duration for high precision ranging, based on multiple symbols of chirp spread spectrum (CSS) is proposed. Since the permissible error of a crystal oscillator in CSS is relatively high given the need to lower device costs, ranging results are perturbed by clock drift. We establish the phenomenon of clock drift in multiple symbols of CSS, and estimate the clock drift in symbol duration based on phase difference between adjacent symbols. The proposed algorithm is analyzed, and verified by Monte Carlo simulations.

The multilevel dual-channel (MLDC) not-AND (NAND) flash memories cell structures with asymmetrically-doped channel regions between the source and the drain were proposed to enhance read and program verifying speeds. The channel structure of the MLDC flash memories consisted of two different doping channel regions. The technical computer aided design simulation results showed that the designed MLDC NAND flash cell with asymmetrically-doped channel regions provided the high-speed multilevel reading with a wider current sensing margin and the high-speed program verifying due to the sensing of the discrete current levels. The proposed unique MLDC NAND flash memory device can be used to increase read and program verifying speed.

In this paper, we describe a verification environment which is based on a constrained random layered testbench using SystemVerilog OOP. As SystemVerilog OOP technique does not allow multiple inheritance, we adopt SystemC to design components of a verification environment which employ multiple inheritance. Then SystemC design unit is linked to a SystemVerilog-based verification environment using SystemVerilog DPI and ModelSim macro. Employing multiple inheritance of SystemC makes the design phase of verification environment simple and easy through source code reusability without corruption due to multi-level single inheritance.

System implementation for e-Government initiatives should be reliable. Unreliable system implementation could, on the one hand, be insufficient to fulfill basic system requirements, and more seriously on the other hand, break the trust of citizens on governments. The objective of this paper is to advocate the use of formal methods in general, the OTS/CafeOBJ method in particular in this paper, to help develop reliable system implementation for e-Government initiatives. An experiment with the OTS/CafeOBJ method on an e-Government messaging framework proposed for providing citizens with seamless public services is described to back up our advocation. Two previously not well-clarified problems of the framework and their potential harm realized in this experiment are reported, and possible ways of revisions to the framework are suggested as well. The revisions are proved to be sufficient for making the framework satisfy certain desired properties.

This paper suggests utterance verification system using state-level log-likelihood ratio with frame and state selection. We use hidden Markov models for speech recognition and utterance verification as acoustic models and anti-phone models. The hidden Markov models have three states and each state represents different characteristics of a phone. Thus we propose an algorithm to compute state-level log-likelihood ratio and give weights on states for obtaining more reliable confidence measure of recognized phones. Additionally, we propose a frame selection algorithm to compute confidence measure on frames including proper speech in the input speech. In general, phone segmentation information obtained from speaker-independent speech recognition system is not accurate because triphone-based acoustic models are difficult to effectively train for covering diverse pronunciation and coarticulation effect. So, it is more difficult to find the right matched states when obtaining state segmentation information. A state selection algorithm is suggested for finding valid states. The proposed method using state-level log-likelihood ratio with frame and state selection shows that the relative reduction in equal error rate is 18.1% compared to the baseline system using simple phone-level log-likelihood ratios.

Attacks using hill-climbing methods have been reported as a vulnerability of biometric authentication systems. In this paper, we propose a robust online signature verification algorithm against such attacks. Specifically, the attack considered in this paper is a hill-climbing forged data attack. Artificial forgeries are generated offline by using the hill-climbing method, and the forgeries are input to a target system to be attacked. In this paper, we analyze the menace of hill-climbing forged data attacks using six types of hill-climbing forged data and propose a robust algorithm by incorporating the hill-climbing method into an online signature verification algorithm. Experiments to evaluate the proposed system were performed using a public online signature database. The proposed algorithm showed improved performance against this kind of attack.