Vasily Desnitsky
email: desnitsky@comsec.spb.ru

Igor Kotenko

Expert Knowledge based Design and Verification of Secure Systems with Embedded Devices

Keywords: embedded security, embedded device design and verification, security components, expert knowledge

The sweeping growth of the amount of embedded devices together with their extensive spread pose extensively new design challenges for protection of embedded systems against a wide set of security threats. The embedded device specificity implies combined protection mechanisms require effective resource consumption of their software/hardware modules. At that the design complexity of modern embedded devices, characterized by the proper security level and acceptable resource consumption, is determined by a low structuring and formalization of security knowledge. The paper proposes an approach to elicit security knowledge for subsequent use in automated design and verification tools for secure systems with embedded devices.

Introduction

The sweeping growth of the amount of embedded devices and their extensive spread pose extensively the problem of design of their protection mechanisms against a wide range of information security threats. Mostly design complexity of secure embedded devices is determined by a low structuring and formalization of the embedded security knowledge. The specificity of the field is appearance of new expert knowledge, their obsolescence, information acquisition from various sources, such as embedded device industry, research and analytical works in information security and software engineering, experience in exploitation of existing information and telecommunication systems, through security and trust analysis of systems. Embedded device specificity, leading to the need of specific approaches to their design and analysis, includes highly specialized purpose of devices and hence the domain specific character of their protection, considerable constraints on volumes of hardware resources, specific sets of vulnerabilities and possible attacks to compromise embedded device and its services, multi-component based approach [START_REF]Object Management Group, The UML Profile for MARTE: Modeling and Analysis of Real-Time and Embedded Systems[END_REF] and therefore possible implicit connections and hidden conflicts between security components arising from the absence of their a priori joint conformity.

As a result, to solve security issues to the full extent information security experts of high qualification are required to be involved in the course of all stages of the design process. In general the search and involvement of such experts complicates the design process significantly, introducing new iterations, feedbacks between the developers, experts and other roles involved as well as increases financial costs to accomplish the development process. At that the current trend in the field of embedded device development is to delegate some part of expert duties to developers, owing to the application of specialized automated techniques and software tools for design, verification, testing, evaluation and implementation of embedded devices. That is knowledge on particular industry systems with embedded devices along with expert knowledge are subjected to generalization and transformed into particular techniques and tools for subsequent application by devices developers.

Another trend in embedded device development is to produce families of devices with a basic functionalities and different extra details determining peculiarities of the device exploitation and finally the cost of the device. As a result there is no necessity to fulfill the expert assisted design process fully for each device within a given family. Instead one should conduct some adaptation of already developed protection procedures and design protection procedures, taking into account the specificity of particular devices that mostly can be delegated to the developer.

The main goal is to form, structure and refine expert knowledge characterizing various design and verification aspects of embedded security mechanisms as well as to search new ones and adopt existing techniques and automated software tools for their subsequent use by developers with embedded devices. The main contribution of the paper is a proposed technique for design and verification on the base of the revealed expert knowledge. The technique is targeted on development of combined security mechanisms for embedded devices, considering resource consumption metrics, possible conflicts and anomalies of security components and information flows. The technique is characterized by engaged specific expert information on hardware resources, typical conflicts and anomalies.

Systems with embedded devices are getting spread in the sphere of home land defense and security. Such systems allow arrangement of collaborative coherent and secure operation of heterogeneous embedded and mobile devices, sensors, servers and other devices as well as various services and agents engaged. Development of security mechanisms for these systems taking into account specificity of particular devices and expert knowledge in the field will facilitate both global and national defense capability.

The paper represents a logical continuation of our published papers on design and analysis of secure systems with embedded devices [START_REF] Desnitsky | Configuration-based approach to embedded device security[END_REF][START_REF] Chechulin | An Approach for Network Information Flow Analysis for Systems of Embedded Components[END_REF][START_REF] Ruiz | A Methodology for the Analysis and Modeling of Security Threats and Attacks for Systems of Embedded Components[END_REF]. Particularly, in the paper we [START_REF] Abraham | Transaction security system[END_REF] propose a heuristic to determine an order of consideration of hardware resources of the configurable device, depending on its functional and non-functional features, (2) extend the list of typical conflicts between security components of embedded devices, (3) reveal relevant types of information flow anomalies and the ways of their detection with reference to information flow analysis inside systems with embedded devices, (4) present the developed software prototype for detection of information flow anomalies, [START_REF] Burleson | Design challenges for secure implantable medical devices[END_REF] fulfill an analysis of the proposed approaches. The rest of the paper is organized as follows. In section 2 the related works are surveyed. Section 3 encompasses the basic elements of the proposed technique, including configuring security components, detection of hidden conflicts, and verification of network information flows. Section 4 comprises the domain specific analysis of the field of embedded security. It outlines a fragment of the case study used as expert knowledge sources for the proposed technique. Section 5 exposes the revealed expert knowledge used in configuration and verification processes. Issues of software implementation and discussion are presented in section 6.

Related works

A multi-component based approach to design systems with embedded devices got a relatively wide application [START_REF]Object Management Group, The UML Profile for MARTE: Modeling and Analysis of Real-Time and Embedded Systems[END_REF] particularly within mobile operating systems Android.

The protection system is represented as a set of interacting software and software/hardware components, each of them being in charge of particular functional security requirements. At that the process for combining security components, taking into account their peculiarities into a single mechanism is configuration of security components [START_REF] Desnitsky | Configuration-based approach to embedded device security[END_REF]. The drawbacks of the approach are possible implicit connections and hidden conflicts between security components arising from the absence of their a priori joint conformity. In [START_REF] Arbaugh | Embedded security: challenges and concerns[END_REF][START_REF] Kocher | Security as a new dimension in embedded system design[END_REF][START_REF] Rae | A Taxonomy of Attacks on Secure Devices[END_REF][START_REF] Grand | Practical Secure Hardware Design for Embedded Systems[END_REF][START_REF] Koopman | Embedded System Security[END_REF] the core problems in the field of embedded device security are presented as particular security domain problems such as user identification, local secure data storage, software resistance to modifications, secure access, side channel attacks protection and others. Contemporary security mechanisms of embedded devices mostly are oriented to particular specific vulnerabilities. In [START_REF] Abraham | Transaction security system[END_REF][START_REF] Kommerling | Design principles for tamper-resistant smartcard processors[END_REF][START_REF] Rae | A Taxonomy of Attacks on Secure Devices[END_REF][START_REF] Ruiz | A Methodology for the Analysis and Modeling of Security Threats and Attacks for Systems of Embedded Components[END_REF] various classifications of vulnerabilities, embedded device intruders are proposed, exposing intruder capabilities, competence and access type. At that combining various heterogeneous protection means within a single device, interrelations between them and issues of their integration correctness are not presented in existing works to the full extent. The importance of the embedded device development, taking into account acceptable energy and computational expenses along with higher security level are uncovered in [START_REF] Dick | High-speed security Embedded security[END_REF][START_REF] Knezevic | Design Methods for Embedded Security[END_REF][START_REF] Ravi | Security in Embedded Systems: Design Challenges[END_REF]. Besides granting necessary hardware and energy resources to the device and its services, a special issue is DoS attacks targeted on exhaustion of device energy resources [START_REF] Moyers | Effects of Wi-Fi and Bluetooth Battery Exhaustion Attacks on Mobile Devices[END_REF][START_REF] Wang | Exposing Security Risks for Commercial Mobile Devices[END_REF]. At that this kind of attacks is not detected by conventional antivirus solutions and other ones, but aimlessly waste energy resources through the use of the most energy expensive hardware components like Wi-Fi and Bluetooth modules or screens, complicating the further functioning of the device. Therefore a complex security mechanism should contain software and hardware modules against various relevant security vulnerabilities, taking into account possible implicit connections and inconsistencies between particular protection modules.

As a way to achieve a tradeoff between the security of the device and its resource consumption, Gogniat et al. [START_REF] Gogniat | Reconfigurable Security Primitive for Embedded Systems[END_REF] propose the usage of reconfigurable security primitives on the base of dynamic adaptation of the device architecture, depending on a state of the device and its environment. The adaptation suggested in [START_REF] Gogniat | Reconfigurable Security Primitive for Embedded Systems[END_REF] is based on, first, dynamic switching between a number of mechanisms integrated in the device and, second, update of these mechanisms.

Configuration processes along with analysis of hardware resource constraints and time expenses are of importance for development of end-products [START_REF] Juengst | Using Resource Balancing to Configure Modular Systems[END_REF][START_REF] Wei | An Approach of Product Configuration Based on Decision Tree and Minimum Conflicts Repair Algorithm[END_REF][START_REF] Yu | A Configuration Tool to Increase Product Competitiveness[END_REF]. At that configuring facilitates a shift from development of a mass product to a customized one adjusted to the needs of a particular client [START_REF] Sabin | Product configuration frameworks-a survey[END_REF].

As design case tools the specific UML profiles are used in the industry, holding relevant embedded security peculiarities, particular requirements, vulnerabilities, security components and their properties and connections between them. In particular in [START_REF] Ruiz | A Methodology for the Analysis and Modeling of Security Threats and Attacks for Systems of Embedded Components[END_REF][START_REF] Ruiz | Security Engineering and Modelling of Set-Top Boxes[END_REF][START_REF] Secfutur | Design of Secure and energy-efficient embedded systems for Future internet applications[END_REF] Domain Specific Models are introduced to model and analyze security mechanisms for systems with embedded devices. In essence each domain is oriented to representation of the device or the whole system in the context of some particular security feature, such as secure storage domain, secure communication domain, user authentication one, etc. An advantage of the approach is delimitation of the design process tasks, responsibilities and roles involved as well as the use of expert knowledge in embedded security field to produce a device protection system. Software tool SPT (SecFutur Process Tool) [START_REF] Secfutur | Design of Secure and energy-efficient embedded systems for Future internet applications[END_REF] implementing the concept of domain specific models represents an extension to general purpose design environment MagicDraw. Model-driven design and analysis of embedded devices and real time systems are presented in MARTE framework [START_REF]Object Management Group, The UML Profile for MARTE: Modeling and Analysis of Real-Time and Embedded Systems[END_REF] defining a complex UML based conception of software and hardware qualities of a device to support its specification, synthesis, verification, validation, performance evaluation, quantity analysis and device certification with the use of UML profiles. However UML based software tools for design and verification are oriented to development of static structure of devices, their specification and subsequent software/hardware implementation without evaluation of dynamically changing characteristics such as resource consumption laying beyond the scope of conventional UML apparatus.

Design and verification approaches

This section presents the basic elements of the proposed technique for design and verification of systems with embedded devices. The technique includes the following stages: (1) configuring security components of an embedded device; (2) verification of its protection system to reveal hidden conflicts; (3) verification of network information flows. The essence of the technique is in the use of specific heuristic based embedded security related knowledge as completed design and verification patterns along with the use of methods of model checking, discrete optimization and decision making.

A. Configuring security components

Correlation of security level of embedded devices and their various non-functional characteristics such as resource consumption represents a challenge in the field of secure embedded device development. Often the absence of effective design-time tools to develop combined security mechanisms complicates or even makes virtually impracticable the implementation of sound protection system. The proposed approach to design the protection systems for embedded devices is realized in accordance with multi-component based approach, taking into consideration both functional and nonfunctional requirements and limitations of the device and security components as well as resource consumption criteria to obtain the most effective solutions customized by non-functional constraints of a particular kind of devices. In essence a resource consumption criterion determines a sequence of hardware resources ordered by their criticality level. At that a discrete optimization problem is formed on a set of security configurations, while its solution allows getting the optimal configuration [START_REF] Desnitsky | Configuration-based approach to embedded device security[END_REF].

The goal of the proposed approach is to determine the most resource effective (optimal) configuration of the protection system on the base of input data on the device and its security components. The configuration is intended to be integrated into the protection system of the device. Finding the optimal configuration will allow ultimately improvement of device protection effectiveness. The choice of an optimal configuration depends on the following factors: (1) device hardware capabilities and volumes of resources to be allotted to support the protection system; (2) needs of the resources for particular security components. For instance asymmetric encryption as a rule requires significant computational expenses; a remote attestation component requires additional network bandwidth expenses leading to higher consumption of energy resources; (3) device peculiarities, scenario of the device, its autonomy, mobility as well as other characteristics and requirements to the device and protection.

Configuring is conducted in automated mode on the base of developed decision making tool to choose optimal configurations. At that, resource consumption criteria are set manually, depending on non-security requirements, peculiarities of the device and its protection system under configuration process. Therefore we propose to use a specific heuristic to determine an order of consideration of hardware resources in the configuration process, depending on functional and non-functional features of the device. Further in sections 4 and 5 in framework of a domain-specific analysis of the field of embedded security we survey shortly a case study as well as a heuristic based on the analysis of this case study. In essence configuring represents a discrete multicriteria optimization problem on the set of security components. Due to the finite and relatively small amount of security component alternatives available in the design process there is no need to look for or create any specific methods to solve the optimization problem in a short period of time. In fact the proposed heuristic should be used by the device developer to form particular optimization problem constraints and their order properly.

B. Detection of hidden conflicts between security components

Multi-component based approach to design of embedded devices and in particular their protection systems cause a problem of correct and secure combined use of several security components. Even assuming individually each security component has no internal inconsistencies and vulnerabilities, the combined protection mechanism nonetheless can be subject to hidden conflicts of different character.

Such conflicts may lead to security vulnerabilities in the protection system, incorrect work of the protection system and even business functions of the device. The main complexity is that these conflicts may appear at the exploitation stage of the device only. Therefore their elimination may require lots of financial costs and industrial expenses. Thus an important task is seen to detect known kinds of hidden conflicts between security conflicts in design-time. In section 4 we present a number of typical conflicts as a piece of expert knowledge and their examples. These conflicts were got heuristically through an analysis of existing systems with embedded devices and a range of papers on embedded security [START_REF] Burleson | Design challenges for secure implantable medical devices[END_REF][START_REF] Secfutur | Design of Secure and energy-efficient embedded systems for Future internet applications[END_REF].

C. Verification of network information flows

The goal of network information flow verification is to evaluate security level of the developed information system with embedded devices. The verification is conducted through checking correctness of the security policy for the system and determine to what extent information flows in the real system correspond to the policy.

By information flow we mean summation of information passed between two or more interacting objects. Information flow security policy represents a set of rules determining which information flows in the system are permitted or prohibited.

Conventionally information flow analysis is conducted at three levels, (1) hardware -as an analysis of ties between the microcircuits [START_REF] Braghin | A model checking-based approach for security policy verification of mobile systems[END_REF], (2) software -as an analysis of the source code running on the device [START_REF] Pistoia | A Survey Of Static Analysis Methods for Identifying Security Vulnerabilities In Software Systems[END_REF], and (3) network -as analysis of network connections in systems with embedded devices. Information flow analysis at these levels are covered in detail in existing literature [START_REF] Pistoia | A Survey Of Static Analysis Methods for Identifying Security Vulnerabilities In Software Systems[END_REF][START_REF] Hedin | A Perspective on Information-Flow[END_REF]. Amount of papers on verification of network information flows is significantly less than ones on software and hardware flows. The concept of information flow is widely used in security evaluation of a route and network effectiveness evaluation [START_REF] Agaskar | Distributed Detection of Multi-hop Information Flows with Fusion Capacity Constraints[END_REF][START_REF] Sprintson | A New Construction Method for Networks from Matroids[END_REF]. Although these studies are not directly related to the types of data transmitted by information flows in the network, but nonetheless, they can be used for modeling information flows. Usually information flows between nodes are specified as a directed acyclic graph. Thus, to reveal covert channels the topological analysis described in [START_REF] Rae | Identifying Critical Components during Information Security Evaluations[END_REF] can be applied to this graph. In this paper we apply model checking to verify security policy rules for information flows. In general, checking correctness of network information flows is an integral part of the design process. Carrying out such verification at the initial design stages provides early detection of contradictions in the security policy and inconsistencies of the information system topology.

Verification of network information flows at the initial design stages represents the static analysis of a system. In contrast to the dynamic analysis including testing of end devices on the basis of attack vectors the proposed verification approach can reduce the number and complexity of actions that need to be repeated after the design errors become fixed. In general, the static approach is to analyze the structure of the information system and its characteristics as system models at different levels of abstraction [START_REF] Kotenko | Verification of Security Policy Filtering Rules by Model Checking[END_REF] (security policies and business logic). To verify the security policy rules regarding checking network information flows we propose to apply model checking, using SPIN tool and PROMELA language. Checking information flows is carried out on a model of the system, since information flow verification on the real network would be much more difficult due to the need to involve specialized equipment, software tools and staff of qualification. Enumerating the policy rules is realized in order of decreasing priority until some rule holds. Prioritization allows organization of more complex management of interrelated policy rules.

Analysis of expert knowledge sources

We used three industrial systems with embedded devices (case study) as a source of expert knowledge in the field of embedded systems [START_REF] Secfutur | Design of Secure and energy-efficient embedded systems for Future internet applications[END_REF], namely a system of remote automated control of energy consumption by consumers (abr. MD), a quickly deployable emergency management system (abr. TMN) and a system providing consumers with digital media services (abr. STB). The choice of these three case studies is determined by their different structure, purposes, functional and security features. The expert knowledge obtained through the analysis of these systems can be generalized and used as a completed design and verification patterns in the development of new systems.

The following patterns, forming the proposed technique, are related to expert knowledge. These are particular security requirements in the shape of functional protection properties and possible alternatives for choosing security components; information on non-security features and internal ties of both an embedded device and its security system to be the base of resource consumption construction; possible types of conflicts that security components are involved in; possible types of information flow anomalies and ways of their detection.

A brief description of the system MD developed by Mixed-mode [START_REF] Secfutur | Design of Secure and energy-efficient embedded systems for Future internet applications[END_REF] is presented below. The system represents a network containing digital trusted electricity meters on the client side, a trusted server and database as well as an infrastructure for communications between devices and their management. The system is characterized by a branched network topology, the presence of technical personnel roles in charge of installation, gauging and support of the system devices as well as a need to protect the devices and software services from malicious users and third parties trying to compromise the system. The system contains trusted sensor modules (TSM) to measure electricity of households (Fig. 1).

Fig. 1.

The system of remote automated control of energy consumption [START_REF] Secfutur | Design of Secure and energy-efficient embedded systems for Future internet applications[END_REF] Measurement data got from each TSM are sent, using the local data bus to a trusted sensor module collector (TSMC). For remote access and control of TSM and TSMC a general-purpose terminal belonging to a general purpose network is used. TSM and TSMC are considered as functional physical modules not necessarily standing alone. However they can be implemented within a single device [START_REF] Secfutur | Design of Secure and energy-efficient embedded systems for Future internet applications[END_REF].

On the base of the analysis of the system specification and models of embedded device intruders the developers have provided the following functional protection properties, each of them being associated with some security component [START_REF] Secfutur | Design of Secure and energy-efficient embedded systems for Future internet applications[END_REF]. These are the integrity of data transmitted to and from the device, in particular, the target data of the current energy consumption on the client side; the integrity of data stored locally on the device; the confidentiality of data transmitted to and from the device; confidentiality of data stored locally on the device; data flow control in accordance with a given security policy; monitoring unauthorized and potentially dangerous action in the system; implementation of protection against unexpected data; presence of data protection from destruction and loss during their transmission or processing due to software failures; presence of a mechanism for safe update of security features; ability to identify compromised and alien devices and components; presence of a mechanism for detection of anomalies in the measured data received from the device; realization of local role based access to the device; continuous integrity monitoring software components of the device.

Non-security TSM related expert knowledge items are as follows: presence of a permanent power source; TSM does not store large amounts of data (only stores the measurement data), data loss is not critical; no complicated calculations (since the main function is reading and transfer of data from the sensor); requirement of timeliness of the business process function; importance of communication services, volumes of business data (measurement data) in the device are small.

The search of typical conflicts and anomalies in the system represents a heuristic analysis of specifications and system models, taking into account already known types of conflicts and anomalies listed in section 5. Specifically for the system MD the policy rules constituting a shadowing anomaly have been analyzed.

Expert Knowledge

A. Configuring security components

An optimal configuration choice is carried out using lexicographic ordering of specified resource consumption criteria. The ordering is based on a heuristic to determine the order of consideration of hardware resources in the configuration process, depending on the functional and non-functional features of the configurable device. The heuristic is based on expert knowledge derived from the analysis of three industrial systems with embedded devices (system MD, TMN, STB).

The heuristic represents a general algorithm for prioritization of hardware resources of an embedded device. A set of signs of embedded devices and the services they provide, having the influence on resource consumption is specified. We introduced a three-point ranking for resources according to their criticality to execution of the target device functions (0 means the resource is noncritical, 1 means low criticality and 2 means high criticality). By experts a rank value is specified for each sign of the core device of each of the three systems in use. Table 1 shows the four types of hardware resources in accordance with the methodology MARTE [START_REF]Object Management Group, The UML Profile for MARTE: Modeling and Analysis of Real-Time and Embedded Systems[END_REF], a set of signs for each of them, references to the analyzed systems that have devices with the regarded signs and the corresponding ranks. Thus, the ranks obtained on the basis of expert evaluation of the analyzed systems are taken as ranks of the signs themselves. Hence these rank values can be used for express ranking of resources of the device by its developer without additional participation of experts.

Thus, in configuring process the device characteristic signs are identified from the list of available ones. After that each resource is assigned a maximum value of rank over all held signs corresponding to a given resource. As a result, the considered hardware resources are ordered according to decreasing their ranks. If two or more resources have the same rank value, the default order <HW_PowerSupply, HW_StorageManager, HW_Computing, HW_Communication> is used. It was defined BY experts as a priori and the typical for the most existing systems. It is assumed if necessary this heuristic may be refined by adding additional signs, resources, analyzed systems and devices to consider as expert knowledge.

B. Hidden conflicts of security components

Analysis of hidden conflicts of security components is an integral part of the effective configuration selection process and is performed by embedded device developer during the protection system design. In essence this is a heuristic analysis aimed at identification of known kinds of hidden conflicts, which the security components of embedded devices are involved in [START_REF] Desnitsky | Configuration-based approach to embedded device security[END_REF].

Generally a conflict is regarded as a relationship between two or more security components and represents a contradiction between the functional of several security components, any their non-functional limitations and/or software/hardware platform of the device. The peculiarity of such conflicts is that as a rule they become apparent under certain conditions only and. Therefore, it is difficult to detect them during testing end devices by the use of attack vectors. Early design-time detection of conflicts in the process of integrating security components will help to reduce the number of iterations of the device development process. Besides for a conflict to be appeared not only the fact of integration of multiple security components with specified security functional is important, the way of their integration is significant as well. Specifically two components with opposite protection features can be in a conflict if they are performed simultaneously and interact within a common hardware/software context, for example, they use share data structure, memory, file, communication channel and so on. Knowledge of known types of conflicts is produced by expert analysis, modeling and development of new information systems with embedded devices. It seems appropriate to keep a list of previously discovered types of conflicts, regarding domain-specific nature of each particular system. As a consequence as the specification of the combined device protection system as well as specifications of considered security components should be analyzed together by the developers for the presence of conflicts from the list. Differences between the nature of each particular conflict, amounts of the involved security components and their protection functional, peculiarities of the components interactions and their integration as well as domain-specific character cause the development of comprehensive classification covering all possible hidden conflicts seems infeasible at the moment. However, in the design process a particular classification of conflicts (e.g. according to the type of the involved objects) can be used as an expert knowledge by the device developer of the protection system to realize a directional search of possible conflicts (Table 2).

Table 2. Types of conflicts between security components

Type 1 -conflict due to a lack of consistency between a security component and the device specification Type 2 -conflict between the protection functions of several security components Type 3 -conflict between several basic components within a complex security component Fig. 2 schematically shows the three types of conflict discussed. Examples of each of the three above conflict types are presented in Table 3.

Fig. 2. Three types of security component conflicts

Resolving such conflicts is individual and determined by the specificity of a particular conflict and its security components involved. As resolution options a revision of one or several security components, changing the way their integration or correcting security requirements can be considered.

Table 3. Examples of expert knowledge on conflicts

Conflict type

Conflict example

Type 1 Security_component = "TPM based secure module for storing confidential customer data"; Safity_requirement = "to double customer data by an extra hardware storage module"; Conflict = "assuming the only TPM in the device the unprotected doubling violates data confidentiality" Type 2 Security_component_1 = "backup component for critical customer data"; Security_component_2 = "component for secure guaranteed deletion of critical customer data after some specific event happens"; Conflict = "inconsistent application of the both components to the same data causes a conflict due to a logical opposite of the their security features" Type 3 Security_requirement = "to implement RAID based redundant and high-performance storage of business data by two (or more) secure hardware units"; Assumption = "the inconsistent parameters of the units (e.g. different capacity of the units or their writing speeds)"; Conflict = "the units are correct themselves, but they do not implement RAID"

C. Network information flow verification

For verification of network information flows the expert knowledge includes instances of security policy anomalies and methods for their detection. Consider one type of anomalies more in detail, "shadowing" anomaly. The presence of this anomaly supposed that a rule never works because there are one or more rules with higher priorities "overlapping" it. This anomaly indicates a probable error in the policy, which should be reviewed. Network information flows and policy rules are specified by the following tuples:

InformationFlow = < host1, host2, user1, user2, interface1, interface2, type >, FilteringRule = < host1, host2, user1, user2, interface1, interface2, type, action >,
where host1, host2 -sending and receiving hosts, respectively; user1, user2 -user sending and receiving user; interface1, interface2 -types of hardware Interfaces of the sender and recipient; type -type of the information flow.

Type of information flow refers to a kind of data that the flow encapsulates. Information flow types by both the kind of transmitted information (e.g., user data, critical data, checksums, encryption keys, security certificate, etc.) and the format which the information is presented in (e.g., unencrypted and encrypted messages, compressed message).

The essence of model checking, applying to anomaly detection consists in iterating states the system can move into, depending on the emerging information flows and responses from the component making decisions on policy based permission or rejection of such requests. When iterating the sequence of actions depends on conditions formulated in a language of linear temporal logic and express correct states of the system [START_REF] Chechulin | An Approach for Network Information Flow Analysis for Systems of Embedded Components[END_REF][START_REF] Kotenko | Verification of Security Policy Filtering Rules by Model Checking[END_REF]. State of the system is determined by a set of variables and state change is caused by concurrent processes running in the system. A process to be executed in the next time is chosen randomly. The system considers all the possible sequences of steps for specific processes and signals potentially incorrect state. After that, the user is given a track, i.e. a sequence of steps leading to an incorrect state of the system with respect to given conditions. Basic input of verification of network information flows includes, first, descriptions of policy rules and, second, the structure of the network in the system description language and detectable types of anomalies.

At the first stage of verification input data is converted into an internal format of the verification system. Then, at a second stage, a general model of the system is built to verify prohibiting and permitting rules for information flows. The model is presented in the form of a finite state machine and initialized by the input data in internal format. In the model the anomalies are expressed by formal statements. According to model checking paradigm these formal statements represent properties of correctness, which violation brings the analyzed system in an incorrect state. At the third stage the general model is verified by a model checker tool. In the verification process all incorrect state of the system are revealed. At the final verification stage the obtained are subjected to interpretation. If any anomaly instances are detected, it is created a description containing situation and the information flow leading to the appearance of the anomaly and its type [START_REF] Kotenko | Verification of Security Policy Filtering Rules by Model Checking[END_REF].

For the case of a shading anomaly the verification includes: (1) generating a set of testing flows (the flows are formed on the basis of the so called "boundary" values of the policy rules, i.e. the flows are constructed through any possible combinations of parameters taken from the rule statements); (2) sequential application of the policy to each information flow; thus each time the rule holds it is marked as held; (3) search on the set of rules to identify rules did not hold even once.

Therefore, verification allows getting a set of results, each of them being a pair <A, (B 1 ,...B n )>, where A represents an anomalous rule, B 1 ,...B n are higher priority rules shadowing it. B 1 ,...B n are isolated by an extra pass of the policy by running those testing flows that meet the conditions of rule A.

Software Implementation and Discussion

A software prototype developed is used within the proposed technique of design and verification of systems with embedded devices. The prototype includes a design-time means for making decisions on choosing optimal configurations and for verification of network information flows. The architecture of the tool for making decisions on choosing optimal configurations on the basis of UML class diagrams is presented in Fig. 3. At the architecture there are its grouped elements in charge of the protected device and its properties; security components; classifications of properties of the device and its individual security components; optimality criteria as well as configuration function of and check of configuration admissibility. This tool includes the following main features: (1) configuration function, that forms an optimal configuration according to the given constraints and a list of security components (function configure); (2) check function for verification of configuration admissibility (function verify).

As practice shows, often in the development of combined protection systems with embedded devices the choice of security components is realized by developers intuitively without any experimental evaluations on an already produced device with integrated protection and without taking into account any design-time system models and heuristics. Experiments on modeling strategy for choosing pseudo optimal sets of security components on the base of greedy algorithms have been realized. The strategy represents a procedure for a sequentially organized choice and refinement of security components of the sought configuration iteratively for each security requirement. In fact, this procedure works successively, for each functional protection property choosing a security component from the available ones that consumes the least amount of hardware resources according to their order determined by the heuristic. The averaged experimental data allow us to deduce that the proposed configuration process results in more effective solutions of combined protection. At that the combined protection effectiveness is meant as achievement of minimal resource consumption of a set of security components providing the given security features. More detailed description of the configuration tool, its performance evaluation as well as fragments of the GUI are given in [START_REF] Desnitsky | Configuration-based approach to embedded device security[END_REF].

The proposed verification of network information flows has been implemented for the analysis of security level of the system of automated control of energy consumption by end customers (system MD) with the following limitations. Due to technical simplifications, a limitation of the implementation is setting parameters of the policy both by defining concrete values or rules (specific hosts, interfaces, users) and by using special identifiers any, defining all possible values for a parameter. Generally it is assumed setting undefined sets of parameters of rules ( in particular as the use of structures such as "all the values, excepting x1, x2, x3"). The policy rules for the MD case study were established based on available system specifications.

Fig. 3. A tool for configuring security components

We performed experiments, introducing shadowing anomaly instances into the policy. These anomalies simulate potential errors in the process of the policy development. During the technique all the instances were revealed. After verification completed the original policy was subjected to corrections, the verification repeated and new policy admitted as free of shadowing anomalies.

A piece of the requirements got from MD case study specification presented below.

"The privacy non-relevant data is generated by and temporarily stored on the trusted meter. It is displayed on the trusted meters local display.  Any user shall be able to read the privacy non-relevant data by using the local interface of the Trusted Meter, and only by using the local interface."

Fig. 4 shows a fragment of a security policy, two policy rules in PROMELA language specifying the given requirement and presenting a shadowing anomaly (rule 0 is presented in lines 82-92, whereas rule 1 is in lines 94-104). In accordance with the location the rule 0 has a higher priority than the rule 1. This anomaly is the result of an incorrect indication of the values of interfaces of the source device (interface1).

Fig. 5 shows a window with a trace from the use of SPIN. In particular, it is shown that the rule 1 is indicated as abnormal. The experiments on modeling a large number of involved objects, roles, data types and permitting/prohibiting rules confirmed the effectiveness of the proposed verification for the design of the automated control system of energy consumption (MD). Since the typical conflicts and anomalies are detected mostly heuristically, it is difficult to deduce about any universal ways to resolve them. Elimination of a conflict/anomaly is determined, first of all, by its context including specific security requirements and assumptions, information security risks, modes of the device, involved security components, used interfaces, etc. To verify network control information flows of a security policy it is not sufficient to use pairwise comparisons of the policy rules only. In fact an analysis of the policy rules holdings in dynamic (i.e. model checking) is needed. In general, compared with the classical network architecture, the specificity of information systems with embedded devices in the task of verification of network information flow contains presence of a branched network topology based on heterogeneous embedded devices with different types of communications and types of hardware/software interface being entry and exit points for information flows, and variability of the structure of such systems throughout its work. An advantage of the proposed verification of information flows is to ensure the system security, assuming the same behavior of the model and the real system. Disadvantages include a large amount of computational resources required to analyze complex models; possible false positives, i.e. warnings on anomalies missing the real system; and incompleteness, as instead of the real system its model is verified.

Conclusion

The paper focused at the technique for design and verification of information systems with embedded devices. It is oriented at development and comprehensive analysis of the combined security mechanisms to protect embedded devices on the basis of resource consumption metrics, potential conflicts and anomalies between protection components and information flows. The technique is based on domain-specific analysis of several case studies and characterized by specific expert information on hardware resources of embedded devices, typical conflicts and anomalies. The technique peculiarities include the use of specialized heuristic knowledge in the field of embedded security as completed design and verification patterns, applying methods of model checking, discrete optimization and decision-making theory.

As future research we are planning to identify and use additional expert knowledge by analysis of specifications new case studies, research papers, technical and analytical reports in the field. It is expected to expand the list of typical conflicts and anomalies and do the further work on SPIN based verification component. Knowledge identified in the research is planned to be organized in an ontological form, using a modeling environment Protégé. The peculiarity of this representation is unification of expert information for its subsequent use by device developers both in decision-making design directly and as input for automated development tools.

Fig. 4 .Fig. 5 .

 45 Fig. 4. Example of rules containing a shadowing anomaly

Table 1 .

 1 A heuristic for choosing resource consumption criteria

	Resource type	Signs of embedded devices and its services	Abbreviation of the systems	Rank
	according to MARTE		with devices of the sign
	HW_PowerSupply	The presence of a permanent power source	MD, STB	0
	(energy consumption	Possibility of replacing the device or battery without	TMN	1
	resource)	damage to the provided services
		Sporadic access to a centralized power supply	TMN	1
		High dependency of the mission goal achievement on	TMN	2
		energy resources
	HW_StorageManager	The device does not store large amounts of data, loss of	MD	0
	(storage resource)	data is not critical
		Storing large amounts of data, loss of data is not	STB	1
		critical
		Storing large or unlimited amounts of data, the loss is	TMN	2
		critical
	HW_Computing	No complex calculations, no requirements of message	-	0
	(computational	delivery timeliness
	resource)	No complex calculations, major timeliness	MD	1
		Complex calculations, minor timeliness	STB	2
		Complex calculations, major timeliness	TMN	2
	HW_Communication	No communications (or they are not obligatory for the	-	0
	(communicational	device services)
	resource)	Importance of communications for the device services,	MD	1
		minor data volumes
		Importance of communications, large data	STB, TMN	2

Acknowledgements. This research is being supported by grants of the Russian Foundation of Basic Research (projects 13-01-00843, 13-07-13159, 14-07-00697, 14-07-00417), the Program of fundamental research of the Department for Nanotechnologies and Informational Technologies of the Russian Academy of Sciences (2.2), by Government of the Russian Federation, Grant 074-U01, the State contract #14.ВВВ.21.0097, the project ENGENSEC of the TEMPUS program and the FP7 SecFutur project.


Shinsaku Kiyomoto
email: kiyomoto@kddilabs.jp

Yutaka Miyake

PrivacyFrost2: A Efficient Data Anonymization Tool Based on Scoring Functions

In this paper, we propose an anonymization scheme for generating a k-anonymous and l-diverse (or t-close) table, which uses three scoring functions, and we show the evaluation results for two different data sets. Our scheme is based on both top-down and bottom-up approaches for full-domain and partial-domain generalization, and the three different scoring functions automatically incorporate the requirements into the generated table. The generated table meets users' requirements and can be employed in services provided by users without any modification or evaluation.

Introduction

Anonymization methods have been considered as a possible solution for protecting private information [START_REF] Ciriani | k-anonymous data mining: A survey[END_REF]. One class of models, called global-recoding, maps the values of attributes to other values [START_REF] Willenborg | Elements of Statistical Disclosure Control[END_REF] in order to generate an anonymized dataset. This paper uses a specific global-recoding model, "full-domain generalization", and an additional process for local optimization. Generally, some anonymous tables are generated from an original table and users select a table from these based on certain requirements for the services that they provide to the public. A challenging issue in the anonymization of tables is to realize an algorithm that generalizes a table according to the requirements of a data user. If the algorithm incorporates the requirements into a generated table and outputs the most suitable table, then evaluation and selection of candidates for anonymous tables are not required when using an anonymous table.

In this paper, we propose an anonymization mechanism that reflects the user's requirements. The mechanism is an extension of PrivacyFrost [START_REF] Tanaka | A user-oriented anonymization mechanism for public data[END_REF][START_REF] Kiyomoto | Privacy Frost: A user-oriented data anonymization tool[END_REF], and hold the same properties that are summarized as follows:

-The mechanism generates an anonymous table that satisfies k-anonymity [START_REF] Samarati | Protecting respondents' identities in microdata release[END_REF], l-diversity-family (l-diversity [START_REF] Machanavajjhala | l-diversity: Privacy beyond kanonymity[END_REF] and recursive (c, l)-diversity [START_REF] Machanavajjhala | l-diversity: Privacy beyond kanonymity[END_REF]). -The mechanism is constructed based on a combination of top-down and bottom-up methods for full-domain generalization, and produces the anonymous table that has the best score in the execution. -After full-domain generalization, the mechanism executes the top-down algorithm on each segment to optimize the anonymous table.

-A user inputs not only a set of generalization boundary constraints, but also priorities for quasi-identifiers as the user's requirements for the anonymous table.

We improve the tool to generate more valuable data. Extensions presented in this paper are:

-A privacy notion, t-closeness [START_REF] Machanavajjhala | t-closeness: Privacy beyond kanonymity and l-diversity[END_REF], is supported for anonymization, and we compare the transaction time with that of k-anonymity and l-diversityfamily cases. -Three different scoring functions can be selected for anonymization. The three scoring functions outputs anonymous tables that have characteristic properties for the selected scoring function; thus, it can be selected according to a requirement for each anonymous table. -A pre-sampling process removes isolated records in order to output a more useful table. To optimize output data, we can use a pre-sampling process before execution of the algorithm.

It realizes fast generation of an anonymous table to reflect a user's requirements and reduce the number of candidates for an anonymous table. The mechanism evaluates the score of a table for each iteration of generalization and selects the best scoring table for the next iteration. After some iterations, the mechanism provides a k-anonymous and l-diverse (or t-close) table that is suited to the user's requirements.

The rest of the paper is organized as follows: Related work is presented in Section 2. Section 3 presents assumed requirements from data users. Our mechanism is presented in Sections 4, 5, and 6. We show evaluation results in Section 7 and conclude this paper in Section 8.

Related Work

Samarati and Sweeney [START_REF] Samarati | Generalizing data to provide anonymity when disclosing information[END_REF][START_REF] Samarati | Protecting respondents' identities in microdata release[END_REF][START_REF] Sweeney | Achieving k-anonymity privacy protection using generalization and suppression[END_REF] proposed a primary definition of privacy that is applicable to generalization methods. A data set is said to have k-anonymity if each record is indistinguishable from at least k -1 other records with respect to certain identifying attributes called quasi-identifiers [START_REF] Dalenius | Finding a needle in a haystack -or identifying anonymous census record[END_REF]. In other words, at least k records must exist in the data set for each combination of the identifying attributes. Clearly any generalization algorithm that converts a database into one with k-anonymity involves a loss of information in that database.

Minimizing this information loss thus presents a challenging problem in the design of generalization algorithms. The optimization problem is referred to as the k-anonymity problem. Meyerson reported that optimal generalization in this regard is an NP-hard problem [START_REF] Meyerson | On the complexity of optimal k-anonymity[END_REF]. Aggarwal et al. proved that finding an optimal table including more than three attributes is NP-hard [START_REF] Aggarwal | Anonymizing tables[END_REF]. Nonetheless, k-anonymity has been widely studied because of its conceptual simplicity [START_REF] Al-Fedaghi | Balanced k-anonymity[END_REF][START_REF] Machanavajjhala | l-diversity: Privacy beyond kanonymity[END_REF][START_REF] Machanavajjhala | t-closeness: Privacy beyond kanonymity and l-diversity[END_REF][START_REF] Wong | α, k)-anonymity: an enhanced k-anonymity model for privacy preserving data publishing[END_REF][START_REF] Truta | Privacy protection: p-sensitive k-anonymity property[END_REF][START_REF] Sun | p + , α)-sensitive k-anonymity: a new enhanced privacy protection model[END_REF]. Machanavajjhala et al. proposed another important definition of privacy for a public database [START_REF] Machanavajjhala | l-diversity: Privacy beyond kanonymity[END_REF]. The definition, called l-diversity, assumes a strong adversary having certain background knowledge that allows the adversary to identify object persons in the public database.

Samarati proposed a simple binary search algorithm for finding a k-anonymous table [START_REF] Samarati | Protecting respondents' identities in microdata release[END_REF]. A drawback of Samarati's algorithm is that for arbitrary definitions of minimality, it is not always guaranteed that this binary search algorithm can find the minimal k-anonymity table. Sun et. al. presented a hash-based algorithm that improves the search algorithm [START_REF] Sun | An efficient hash-based algorithm for minimal k-anonymity[END_REF]. Aggarwal et al. proposed the O(k)-approximation algorithm [START_REF] Aggarwal | Approximation algorithms for k-anonymity[END_REF] that is used for executing the k-anonymity problem. A greedy approximation algorithm [START_REF] Lefevre | Mondrian multidimensional kanonymity[END_REF] proposed by LeFevre et al. searches for the optimal multi-dimensional anonymization. A genetic algorithm framework [START_REF] Iyengar | Transforming data to satisfy privacy constraints[END_REF] was proposed because of its flexible formulation and its ability to find more efficient anonymizations. Utility-based anonymization [START_REF] Xu | Utility-based anonymization using local recoding[END_REF][START_REF] Xu | Utility-based anonymization for privacy preservation with less information loss[END_REF] makes k-anonymous tables using a heuristic local recoding anonymization. Moreover, the k-anonymization problem is viewed as a clustering problem. Clustering-based approaches [START_REF] Byun | Efficient k-anonymity using clustering technique[END_REF][START_REF] Truta | K-anonymization incremental maintenance and optimization techniques[END_REF][START_REF] Lin | An efficient clustering method for k-anonymization[END_REF][START_REF] Zhu | Achieving k-anonymity via a density-based clustering method[END_REF] search a cluster that has k-records. In full-domain generalization, there are two heuristic approaches for generalization algorithms: the top-down approach and the bottom-up approach. Bayardo and Aggrawal proposed a generalization algorithm using the top-down approach [START_REF] Bayardo | Data privacy through optimal k-anonymity[END_REF]. The algorithm finds a generalization that is optimal according to a given fixed cost metric for a systematic search strategy, given generalization hierarchies for a single attribute. Incognito [START_REF] Lefevre | Incognito: Efficient full-domain k-anonymity[END_REF] is a bottom-up-based algorithm that produces all possible k-anonymous tables from an original table.

There are several research papers about k-anonymization based on a data owner's requirements for anonymized public data. Loukides et al. considered a k-anonymization approach [START_REF] Loukides | Towards preference-constrained kanonymisation[END_REF] according to both the data owner's policies and data user's requirements. Aggarwal and Yu discussed a condensation based approach [START_REF] Aggarwal | On variable constraints in privacy preserving data mining[END_REF] for different privacy requirements. LeFevre et al. provides an anonymization algorithm [START_REF] Lefevre | Workload-aware anonymization[END_REF] that produces an anonymous view appropriate for specific data mining tasks. Xiao and Tao proposed the concept of personalized anonymity and presented a generalization method [START_REF] Xiao | Personalized privacy preservation[END_REF] that performs the minimum generalization for the requirements of data owners. Miller et al. presented an anonymization mechanism [START_REF] Miller | Constrained k-anonymity: Privacy with generalization boundaries[END_REF] that provides k-anonymous tables under generalization boundaries of quasi-identifiers. The configuration of the boundaries can be considered to be user requirements. We proposed an anonymization mechanism [START_REF] Tanaka | A user-oriented anonymization mechanism for public data[END_REF][START_REF] Kiyomoto | Privacy Frost: A user-oriented data anonymization tool[END_REF] to reflect user requirements precisely. However, the mechanism only provides a basic scoring function for the anonymization and a remaining issue is to design appropriate scoring functions for achieving several requirements on anonymous tables. This paper presents an extension of that mechanism that includes presampling and some scoring functions.

Requirements

A database table T in which the attributes of each user are denoted in one record is in the public domain and an attacker obtains the table and tries to extract the record of an individual. Suppose that a database table T has m records and n attributes {A 1 , . . . , A n }. Each record a i = (a i 1 , . . . , a i n ) can thus be considered to be an n-tuple of attribute values, where a i j is the value of attribute A j in record a i . The database table T itself can thus be regarded as the set of records T = {a i : 1 ≤ i ≤ m}. In our system, a user can input the following conditions for the anonymization.

-Priority. The user defines a positive integer value v a i for each attribute a i . The value depends on the priority of the attribute. That is, v a i = mv a j , where the priority of the attribute a i is m-times higher than a j . For example, the user can define (v a 1 , v a 2 , v a 3 , v a 4 ) = (10, 5, 1, 1). The user gives high priority to an attribute when the user desires more detailed information about the attribute. -Minimum Level. The user can define a minimum level for each attribute.

Each attribute has a hierarchical tree structure. The minimum level w M a i defined by the user means that a k-anonymized dataset generated by the system includes at least w M a i -level information for the attribute. The system does not generalize the attribute below the minimum level.

The above two requirements reflect the granularity of information in a generated anonymous table. The mechanism tries to keep attribute values located at the lower node as much as possible in the generalization hierarchy while satisfying the predefined anonymity condition, when the user marks the attribute as high priority. Furthermore, the user controls the limits of generalization using a configuration of minimum levels for attributes.

Components

In this section, we explain the basic components of our anonymization method.

Generalization

Full-domain generalization for obtaining an anonymous table consists of replacing attribute values with a generalized version of those values, and it is based on generalization hierarchies [START_REF] Ciriani | k-anonymous data mining: A survey[END_REF]. A quasi-identifier is an attribute that can be joined with external information to re-identify individual records with sufficiently high probability [START_REF] Dalenius | Finding a needle in a haystack -or identifying anonymous census record[END_REF]. Generally, a target table T x = (T q |T s ) consists of two types of information: a subtable of quasi-identifiers T q and a subtable of sensitive attributes T s . Since the sensitive attributes represent the essential information with regard to database queries, a generalization method is used to modify (anonymize) T q in order to prevent the identification of the owners of the sensitive attributes, while retaining the full information in T s . Thus, the generalization algorithm focuses on the subtable of quasi-identifier T q and modifies it to satisfy a predefined anonymity condition. We assume that quasi-identifier attributes are known information for the generalization algorithm.

The full-domain generalization modifies all values of the attribute in the table T . Therefore, the anonymized table is not optimized for regional groups that have the same quasi-identifier T q and that have lost information due to the global generalization of attributes. The partial-domain generalization replaces the values of an attribute in a small group that has the same quasi-identifier T q . The partial-domain generalization executes [on] each group independently and modifies T q subject to the requirement that each group satisfies the predefined anonymity condition. Thus, values of the attribute are generalized as values with different levels for each group.

Top-Down and Bottom-Up

There are two methods for generating anonymous tables in generalization schemes: the top-down approach and the bottom-up approach. The top-down approach starts at the root table where all attributes have a root value (a maximally generalized value), and finds an anonymous table to change attribute values to lower values (more detailed values) of the generalization hierarchy. In contrast, the initial table in the bottom-up approach is an original table and attribute values are replaced using upper attribute values until an anonymous table is found. Our scheme uses a top-down approach as the basic algorithm to reduce the number of score calculations. Furthermore, we consider a pre-computation in the top-down approach in order to skip some computations by starting at the root table. The details of our scheme are described in a later section.

Functions

The mechanism generates an anonymous table T G and calculates its score s based on input data: a table T = T q that consists of m records and n quasiidentifiers a i (i=1, ...,n), the parameters for k, a generalization hierarchy for the attributes H a i , the lowest levels w L a i of H a i and the user's requirements v a i and w M a i . The parameters for k are the requirement for privacy (which means kanonymity) and a system parameter that is defined according to the target table.

The score s provides a rating of the degree to which the user's requirements are satisfied. The following subfunctions are used in the algorithm:

-Sort(T, v a 1 , ..., v a n ). This function sorts attributes a i (i = 1, ..., n) in Table

T by the user-defined priority values v a i . The function generates T = (a 1 , ..., a n ) in an order such that v a 1 is the smallest and v a n is the largest. -Check k,l,c,t (T ). This function calculates the minimum number of group members, where T = (T q |T s ) and all records in T q are categorized into groups with the same attribute values. That is, this function calculates x of xanonymity for T q . The function calculates l and c of (c, l)-diversity for T s , or calculates t for t-closeness for T s . The function outputs OK where T satisfies k-anonymity, (c, l)-diversity, and otherwise outputs N G. The function skips calculations for l-diversity where l is defined as 1, and it only executes ldiversity calculations for (c, l)-diversity where c is defined as 0. The function skips calculations for t-closeness where t = -1. First, the function generates the hash value of each record in the table T q and counts the number of hash values that are the same. If all hash values are greater than x, the function outputs x. This process is a simple and efficient way for checking kanonymity and is similar to the process adopted in the previous study. This function is implemented as a modifiable module; we can add other checking logics for anonymity definitions. -Generalization(a i , H a i , w a i ). This function modifies the attribute a i based on its generalization hierarchy H a i . The attribute values change to the upper node values of level w a i -1 , where the level of the attribute value is w a i . -De-Generalization(a i , H a i , w a i ). This function modifies the attribute a i based on its generalization hierarchy H a i . The attribute values change to the lower node values of level w a i +1 , where the level of the attribute value is w a i . -Score(T ). This function calculates the score of a table T . Our system calculates the score S t of the anonymized datasets using equations described in Section 6.

Algorithm

In the generated table, information that is important for the user is maintained at a level that is as detailed as possible, while other information remains at the level of generalized information. The algorithm consists of two main parts: pre-computation and top-down generation.

Pre-Sampling

To optimize output data, we can use a pre-sampling process before execution of the algorithm. The pre-sampling process finds isolated records having attribute sets that very few records have, and removes the isolated records to output more useful tables. If the isolated records are included in a table, other records tend to be much generalized than expected, so deletion of the records helps to keep the maximum amount of information in the table. The pre-sampling process is an optional process that the user can choose to use, or not. Let u = u a 1 , ..., u a n be a threshold level of generalization for each attribute a i , and k ′ be a threshold value of anonymization. When the user inputs a table T , and threshold values u and k ′ , the pre-sampling process is executed as follows:

The algorithm uses the updated table T for generating the anonymous table T G . The whole mechanism is described in Figure 1.

Each attribute a

Pre-Computation

The mechanism uses pre-computation to reduce the total computational cost of anonymization. The pre-computation consists of two steps; step 1 considers single attribute anonymity and generalizes each attribute to satisfy (k + p)-anonymity, and step 2 considers the whole table to satisfy k-anonymity. The parameter p is a system parameter, and it should be optimized according to the results of previous trials. The pre-computation is based on the subset property theorem [START_REF] Lefevre | Incognito: Efficient full-domain k-anonymity[END_REF]. This theorem means that each single attribute has to satisfy k-anonymity for a k-anonymous table. The mechanism uses the top-down approach and starts with a k-anonymous table as the initial table; thus the algorithm executes the following pre-computation.

1. The algorithm generalizes each attribute of a table T (= T q ) to satisfy (k+p)anonymity, and creates a modified table T .

The algorithm checks whether the whole table T satisfies k-anonymity and (c, l)-diversity (or t-closeness). If the table T does not satisfy k-anonymity

and (c, l)-diversity (or t-closeness), then the algorithm generalizes each attribute once (one level) and returns to step 2. Note that each attribute is not generalized up to the minimum level defined by the user. If the algorithm finds no table that satisfies k-anonymity and (c, l)-diversity (or t-closeness), then the algorithm outputs failed. Otherwise, the algorithm makes an initial anonymous table T I and inputs it to T G .

Top-Down Generalization

The basic steps of top-down generalization are as follows:

1. First, the algorithm de-generalizes an attribute a n in Table T The basic algorithm calculates the scores of all possible anonymous tables. Now, we consider a more efficient method for reducing the computational costs of anonymity checks and score calculations. Suppose that the algorithm obtains the number b w a i of nodes at the same level w a i in the generalization hierarchy H a i . The number indicates the upper bound of e a i in each level. Thus, we estimate the upper bound of increase in the score to calculate δ s = (b

w a i +1 -e a i )v a i ,
where the current generalization level of a i is w a i . If s > s ′ + δ s , the algorithm can skip de-generalization of a i . Figure 1 shows the basic algorithm that outputs T G and s using input parameters. The algorithm first executes pre-computation and generates an initial table T I ; then the algorithm searches the table T G that has the highest score. The top-down approach is used for the search performed by the basic algorithm.

Optimization Steps

We present optimization steps to find a better table that has a higher score than the table found using the basic algorithm. The optimization consists of three steps: the second top-down, bottom-up, and partial-domain de-generalization. The extension part is executed after the execution of the basic algorithm. The algorithm repeats two sub-functions until no table has a score higher than the current best score; then the algorithm executes the partial-domain generalization process, if required. An overview of the search process is shown in Figure 2. The figure is a generalization graph of the table T and the top is a root table in which all attributes are level 0. The extended algorithm tries to find a table using both top-down and bottom-up approaches. The algorithm searches for the high-score table on the boundary of anonymous tables and tables that do not satisfy the predefined anonymity condition. The extended algorithm is executed after the basic algorithm as follows:

1. After the basic algorithm, the algorithm generalizes possible a i s in the table T G and calculates the scores of the tables. Then, the algorithm selects the top score table T T . Note that table T T does not satisfy Check k,l,c (T ) = OK. 2. Next, the algorithm executes a bottom-up generalization to search for tables that satisfy the predefined anonymity condition, then from these tables the algorithm chooses the table with the best score. 3. The algorithm compares the score of the chosen table with the current score s of table T G , and if the score is higher than s, the algorithm replaces T G with table T and s by its score. The algorithm executes the above steps using the new T G . Otherwise, the algorithm stops and outputs the current generalized table T G . The steps of top-down and bottom-up are repeated until no table has a score higher than the current best score. 4. After finding the best score table, the algorithm executes the top-down approach for each partial-domain using a function named "Partial-Domain De-Generalization (T )". The function selects one group that has the same quasiidentifiers and modifies one attribute using the top-down approach to satisfy the predefined anonymity condition. The algorithm executes the function until the table T T does not satisfy Check k,l,c (T ) = OK. Note that the partialdomain generalization process consists of only the top-down approach, and the score of the output table is larger than that of the best scoring table produced by full-domain generalization. This step is optional; the user decides whether the partial-domain generalization process is executed for the table.

Details of the algorithm are shown in the Appendix.

Scoring Functions

In this section, we explain scoring functions that are used in the anonymization algorithm.

Basic Scoring Function

The basic function is described as follows:

St = ∑ ∀a i v a i • e a i
where e a i is the number of value types of an attribute a i in the table. The score is high where the user-defined priority value for the attribute is high and the attribute has many types of values. The function produces a single value; thus, different priority values may produce the same value. The function is implemented as a replaceable module; thus, we can adjust the function or add another scoring function according to data types. Note that the table with the best score is not optimal among k-anonymous tables, but is suitable for the user's requirements.

η-Based Scoring Function

The η-based scoring function focuses on the variation of attribute values for all attributes (calculated as the sum of e a i ) more than in the case that we use the basic scoring function. Thus, the table tends to be uniformly generalized. The η-based scoring function is described as follows:

St = ∑ ∀a i v a i • η(e a i )
The function η(x) is defined as:

η(x) =      2 x > d 1 d 2 < x ≤ d 0 x ≤ d 2
Where d is a constant parameter. We can extend the function η(x) to add conditions for x.

Logarithm-Based Scoring Function

The logarithm-based scoring function focuses on the priorities (defined as v a i ) more than on the basic scoring function. In particular, the precision of the toppriority attribute is of prime importance in the generalization. The logarithmbased scoring function is described as follows:

St = max ∀a i v a i • log(e a i ) log(e b a i )
where e b ai is the value of e ai before anonymization. Figure 2 shows two tables generated by the η-based scoring function and the logarithm-based scoring function, respectively. The left table is generated using the logarithm-based scoring function with a priority that the attribute "Nationality" is the most valuable attribute in the table.

Performance Evaluation

We implemented a prototype system on a PC (Core i7 870 2.93 GHz, 4 GB Memory, Windows 7, 32 bit) and evaluated the transaction times for pre-sampling and anonymization. In this section, we show the results of the experiments.

We evaluated the prototype system using two data sets [START_REF] Asuncion | UCI machine learning repository[END_REF], Adults Data Sets, which has 32,561 records of 14 attributes, and Census-Income Data Sets, which has 199,523 records of 42 attributes, under several different sets of parameters k, l and c. These data sets had been used for performance evaluation in previous research. The transaction time for pre-sampling is shown in Table 1. The All threshold level of generalization for each attribute a i was configured as 2 in the experiments. The All transaction time for Adults Data Sets was about 1.2 seconds and that for Census-Income Data Sets was about 4.4 seconds. The transaction times for anonymization for Adults Data Sets and Census-Income Data Sets are shown in Table 2 and Table 3, respectively. In all experimenst, we measured transaction time including the partial-domain de-generalization steps. The transaction time when using t-closeness was almost same as that when using l-diversity. There were no significant differences between the three scoring functions.

Thus, our prototype system is expected to generate anonymous tables in a feasible transaction time. In particular, where the table has fewer than 30,000 records and each consists of a reasonable number of attributes, the prototype system will generate an anonymous table for it in real-time.

Conclusion

In this paper, we proposed an anonymization scheme for generating a table with k-anonymity. The scheme calculates the scores of intermediate tables based on user-defined priorities for attributes, and from these it selects the table with the highest score. Three scoring functions were designed and they can be selected according to the specific requirements of each case.

Fig. 1 .

 1 Fig. 1. Mechanism Overview

Fig. 2 .

 2 Fig. 2. Generated Anonymous Tables

Fig. 3 .

 3 Fig. 3. Algorithm

  i is generalized up to the level u a i and the process outputs a temporary generalized table T P . 2. Using table T P , the process makes groups whose records have the same attribute sets, and counts the number of records in each group. The process picks up records that belong to a group having records less than k ′ . 3. The selected records are removed from the original table T . The process outputs the updated table T . Note that the generalized table T P is just discarded.

	T
	Pre-Sampling
	(Optional)
	Algorithm
	Pre-Computation
	Top-Down
	2 nd Top-Down
	Bottom-Up
	Partial-Domain De-Generalization
	(Optional)
	T G , Score

  G , which is defined as a top priority by the user, then checks the k-anonymity and (c, l)diversity (or t-closeness) of the modified tableT. 2. If the table satisfies the predefined anonymity condition, the algorithm calculates the score of the modified table T . If the algorithm finds no table that satisfies the predefined anonymity condition, then the algorithm outputs the table T G and its score s. The score is computed using the scoring function Score(T ). 3. For all possible modifications of a i (i = 1, ..., n), the algorithm checks kanonymity and (c, l)-diversity (ort-closeness), then calculates the scores. The algorithm selects the table that has the largest score among the possibly anonymous tables and executes step 1 again. 4. If no more tables satisfy the predefined anonymity condition, the algorithm outputs the table that has the maximum score at that point.

Table by -

 by Based Scoring Function Table by Logarithm-Based Scoring Function

		Quasi-Identifiers			Quasi-Identifiers
	Birth	Gender	Zip Nationality	Birth	Gender	Zip Nationality
	198*	*	012**	UK	1984	Male	0124*	Europe
	198*	*	012**	Italy	1984	Male	0124*	Europe
	198*	*	012**	UK	1985	Female 0123*	Europe
	198*	*	012**	Italy	1985	Female 0123*	Europe
	1984	Male	0123*	USA	1984	Male	0123*	USA
	1984	Male	0123*	USA	1984	Male	0123*	USA

Table 1 .

 1 Transaction Time of Pre-Sampling

	Data	No. of k ′ Transaction
		Records	Time
	Adult	32,561 1 1289 ms
	Adult	32,561 2 1299 ms
	Adult	32,561 5 1307 ms
	Adult	32,561 10 1286 ms
	Census-income 199,523 1 4401 ms
	Census-income 199,523 2 4324 ms
	Census-income 199,523 5 4431 ms
	Census-income 199,523 10 4464 ms

end if end for if state

  The generated table meetsInput: a table T , k, l, c, t, p, H a i , w L a i , v a i , w M Sort (T, v a 1 , ..., van )for i = 1 to n do w a i ← w L a i while Check(a i ) < k + p do a i ← Generalization(a i , H a i , w a i ) w a i ← w a i -1 end while end for while Check k,l,c (T ) = N G and all w a i > w M a i do for i = 1 to n do if w a i ≥ w M a i then a i ← Generalization(a i , H a i ) w a i ← w a i -1 = f alse then state ← stop end if a 1 , ..., a n , v a 1 , ..., van ← temp end while return T G , s repeat // 2nd Top-Down: T ′ ← T G s ′ ← s state ← f alse for i = n to 1 do T ← T ′ a i ← De-Generalization(a i , H a i , w a i ) if Score(T ) > s ′ then temp ← a i , w a i + 1 T Bottom-Up: while Check k,l,c (T ) = N G do T ′ ← T T state ← f alse a 1 , ..., a n , v a 1 , ..., van ← temp for i = 1 to n do T ← T ′ if w a i > w M a i then a i ← Generalization(a i , H a i , w a i ) end if if Check k,l,c (T ) = OK and Score(T ) > s then temp ← a i , w a i -1 T ′ if w a i > w Ma i then a i ← Generalization(a i , H a i , w a i )

	a i
	(i=1, ..., n), Score F unction
	Output: T G , s
	// *Pre-Sampling before Algorithm (Optional) // // Precomputation: end if end for end while T I ← T T G ← T I s, s ′ ← Score(T ) if Check k,l,c (T ) = N G then return f ailed end else Top-Down Generalization // Top-Down Generalization: while state ̸ = stop do T T ← T s T ← Score(T ) state ← true end if end for if state = f alse then state ← stop return T G , s else // end if if Score(T ) > s ′ then
	T T ← T temp ← a i , w a i -1 s ′ ← Score(T )
	state ← true end if end for if state = f alse then
	state ← stop
	end if end while until state = stop
	// Partial-Domain Generalization:
	while Check k,l,c

′ ← T G s ′ ← s state ← f alse for i = n to 1 do T ← T ′ a i ← De-Generalization(a i , H a i , w a i ) if Check k,l,c (T ) = OK and Score(T ) > s then temp ← a i , w a i + 1 T G ← T s ← Score(T ) state ← true G ← T s ← Score(T )

state ← true end if end for if state = true then a 1 , ..., a n , v a 1 , ..., van ← temp else for i = 1 to n do T ← T

PrivacyFrost2

user's requirements and is employed in the services provided by users without any modification or evaluation. Our mechanism is applicable to full-domain and partial-domain generalization in some types of anonymity definitions to replace the check function. We will evaluate the prototype system using a number of tables for several users requirements, and consider an optimization method for parameters in our future work.