摘要：Numerous Internet security incidents have shown that support from secure operating systems is paramount to fighting threats posed by modern computing environments. Based on the requirements of the relevant national and international standards and criteria, in combination with our experience in the design and development of the ANSHENG v4.0 secure operating system with high security level （hereafter simply referred to as ANSHENG OS）, this paper addresses the following key issues in the design of secure operating systems with high security levels： security architecture, security policy models, and covert channel analysis. The design principles of security architecture and three basic security models： confidentiality, integrity, and privilege control models are discussed, respectively. Three novel security models and new security architecture are proposed. The prominent features of these proposals, as well as their applications to the ANSHENG OS, are elaborated. Cover channel analysis （CCA） is a well-known hard problem in the design of secure operating systems with high security levels since to date it lacks a sound theoretical basis and systematic analysis approach. In order to resolve the fundamental difficulties of CCA, we have set up a sound theoretical basis for completeness of covert channel identification and have proposed a unified framework for covert channel identification and an efficient backward tracking search method. The successful application of our new proposals to the ANSHENG OS has shown that it can help ease and speedup the entire CCA process.

摘要：Various extensions of UML have been developed to meet the challenges of designing modern software systems, such as agent based electronic commerce applications. Recent advances in model checking technology have led it to be introduced into the development of approaches and tools to check the correctness of electronic commerce protocols. This paper focuses on the research of a method that connects an extension of AUML to model checker SPIN/Promela for the specification and verification of agent interaction protocols (AIP) in electronic commerce. The method presented here allows us to combine the benefits of visual specification with the power of some static analysis and model checking. Some algorithms and rules are developed to permit all visual modeling constructs translated mechanically into some Promela models of AIP, as supported by the model checker SPIN. Moreover, a process is illustrated to guide the specification and verification of AIP. The method is demonstrated thoroughly using the e commerce protocol NetBill as an example.

摘要：Based on the origin of message items and channel combination between transacting parties, and events and relations among events, this paper presents a concise, precise, and hierarchical model for general fair exchange protocols, formally specifies various security requirements which are able to reflect inherent requirements for fair exchange protocols more rigorously, and partition these security requirements with fine granularity. This work helps analyze, debug, and design multi-party fair exchange protocols more effectively and elaborately,

摘要：Formal verification of VHSIC Hardware Description Language （VHDL） in Field-Programmable Gate Array （FPGA） design has been discussed for many years. In this paper we provide a practical approach to do so. We present a semi-automatic way to verify FPGA VHDL software deadlocks, especially those that reside in automata. A domain is defined to represent the VHDL modules that will be verified; these modules will be transformed into Verilog models and be verified by SMV tools. By analyzing the verification results of SMV, deadlocks can be found; after looking back to the VHDL code, the deadlocking code is located and the problem is solved. VHDL verification is particularly important in safety-critical software. As an example, our solution is applied to a Multifunction Vehicle Bus Controller （MVBC） system for a train. The safety properties were tested well in the development stage, but experienced a breakdown during the long-term software testing stage, which was mainly caused by deadlocks in the VHDL software. In this special case, we managed to locate the VHDL deadlocks and solve the problem by the FPGA deadlock detection approach provided in this paper, which demonstrates that our solution works well.

摘要：FGSPEC is a wide spectrum specification language intended to facilitate the software specification and the expression of transformation process from the functional specification which describes“what to do”to the corresponding design(operational)specification which describes“how to do”.The design emphasizes the coherence of multi-level specification mechanisms and a tree structure model is provided which unifies the wide spectrum specification styles from“what”to“how”.

摘要：Early Java implementations relied on interpretation, leading to poor performance compared to compiled programs. Java just-in-time (JIT) compiler can compile Java programs at runtime, so it not only improves Java's performance prominently, but also preserves Java's portability. In this paper the design and implementing techniques of Java JIT compiler based on Chinese open system are discussed in detail. To enhance the portability, a translating method which combines the static simulating method and macro expansion method is adopted. The optimization technique for JIT compiler is also discussed and a way to evaluate the hotspots in Java programs is presented. Experiments have been conducted to verify JIT compilation technique as an efficient way to accelerate Java.

摘要：Recently service orientation is becoming a mainstream approach for building large scale software systems. A key requirement in service-oriented design is the dependability of service. It stipulates that the behavior of services is controllable. Formal models can aid in constructing software in a dependable manner. They can describe ser- vices precisely and compose them together consistently. This paper presents a strategy for service realization based on a novel layered formal model. When a service is provided or required via internet, the semantic consistency becomes critical issue, Our architecture tackles the issue by proposing a novel scheme： defining contract of a service to keep semantic information. Although service-oriented design is our prime target, the contract models, to a large extent, are independent of the framework of design and therefore applicable to large scale software design in general.

摘要：Some testing results on DAWNING-1000, Paragon and workstation cluster are described in this paper. On the home-made parallel system DAWNING-1000 with 32 computational processors, the practical performance of 1.117 Gflops and 1.58 Gflops has been measured in solving a dense linear system and doing matrix multiplication, respectively. The scalability is also investigated. The importance of designing efficient parallel algorithms for evaluating parallel systems is emphasized.

摘要：In this paper, a general framework for designing and analyzing password-based security protocols is presented. First we introduce the concept of ＂weak computational indistinguishability＂ based on current progress of password-based security protocols. Then, we focus on cryptographic foundations for password-based security protocols, i.e., the theory of ＂weak pseudorandomness＂. Furthermore, based on the theory of weak pseudorandomness, we present a modular approach to design and analysis of password-based security protocols. Finally, applying the modular approach, we design two kinds of password-based security protocols, i.e., password-based session key distribution （PSKD） protocol and protected password change （PPC） protocol. In addition to having forward secrecy and improved efficiency, new protocols are proved secure.

摘要：Viral advertising in social networks has arisen as one of the most promising ways to increase brand awareness and product sales. By distributing a limited budget, we can incentivize a set of users as initial adopters so that the advertising can start from the initial adopters and spread via sociM links to become viral. Despite extensive researches in how to target the most influential users, a key issue is often neglected： how to incentivize the initial adopters. In the problem of influence maximization, the assumption is that each user has a fixed cost for being initial adopters, while in practice, user decisions for accepting the budget to be initial adopters are often probabilistic rather than deterministic. In this paper, we study optimal budget allocation in social networks to maximize the spread of viral advertising. In particular, a concave probability model is introduced to characterize each user＇s utility for being an initial adopter. Under this model, we show that it is NP-hard to find an optimal budget allocation for maximizing the spread of viral advertising. We then present a novel discrete greedy algorithm with near optimal performance, and further propose scaling-up techniques to improve the time-efficiency of our algorithm. Extensive experiments on real-world social graphs are implemented to validate the effectiveness of our algorithm in practice. The results show that our algorithm can outperform other intuitive heuristics significantly in almost all cases.