Andreas Fuchs

Christoph Krauss

Jürgen Repp

Christoph Krauß

Runtime Firmware Product Lines using TPM2.0

des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

The development of Information Technology (IT) products has shifted drastically from separate and designated designs per model to unified hardware architectures with different software versions. Different products of similar kind nowadays only differ by their casing and firmware -and sometimes additional interfaces. For example, an Original Equipment Manufacturer (OEM) may produce routers and firewalls that only differ in the casing, firmware, and number of network ports. The firmware, however, differentiates a router from a firewall.

To improve the software production process, software product lines [11] were introduced for generating similar software versions at compile-time from a shared set of software components using conditional compilation techniques, e.g., #ifdef in the C programming language or flags such as --enable-feature[=arg] in the GNU Autoconf package [START_REF]GNU: Autoconf[END_REF]. Firmware product lines are used for generating unified firmware source code for (embedded) systems, e.g., by using the Open-Embedded software framework [7] to generate a customized Linux distribution.

The next iteration of device product lines will go even beyond this and we refer to this step as runtime firmware product lines. Instead of compiling and packaging different firmware images from the same code collection, a unified firmware image will be delivered for a whole product series. The product customization will happen on the device itself. Hence, one firmware image contains several features and the device itself "decides" whether to unlock a certain feature or not. We use overlay mounting for the unlocking of features. This approach is particularly attractive due to its cost efficiency and simplifies the maintenance of devices drastically. However, it poses the risk that attackers could alter their model and upgrade it to a higher-level model.

In this paper, we propose an approach for secure runtime firmware product lines enabling the provisioning of unified firmware images to a whole series of products while preventing unauthorized feature activation by an attacker. Our approach uses the Trusted Platform Module (TPM) 2.0 to protect the intellectual property and model feature sets while still enabling refurbishment by changing the concrete model assignment. The general idea is using the TPM as a security anchor to individually encrypt the different features and controlling access to these features using some of the new TPM 2.0 functionalities such as enhanced authorization. Using our approach, development and firmware update processes are eased drastically by enabling unified firmware provisioning for complete model series which is also shown by our proof-of-concept implementation.

General Idea

In our approach, a device is equipped with a TPM 2.0 that can be a dedicated hardware chip but also a software implementation to save costs. The TPM acts as security anchor by providing secure storage, secure execution, and additional features for controlling access (cf. Section 3.3).

The general idea of our approach is as follows. A unified firmware image for a product line consists of several separate read-only feature filesystems. Each feature filesystem contains a specific feature set and is encrypted using a unique cryptographic feature key. For each model of a product line, a different model number is stored inside the devices' TPM. This TPM-resident model number serves as a basis of the runtime configuration of the firmware image to be booted. By verifying a TPM-Policy, only the allowed features for a specific model of a product line are unlocked, i.e., decrypted. Note that accessing the unified firmware image is only possible on an original OEM device containing the preconfigured TPM. If required, additional read-write filesystems for local data localdataFS (e.g., for /etc, /home, /srv) and temporary files tmpFS (e.g., for /var) can be mounted. The protection of the localdata filesystem against manipulation is out of scope of this paper, but can be easily realized, for example, using the approach presented in [START_REF] Fuchs | Advanced remote firmware upgrades using TPM 2[END_REF].

Fig. 1 shows an example to illustrate our approach in more detail. The unified firmware image is structured by the means of overlay read-only filesystems. A base file system BaseFS contains those parts that are shared between all models. It includes the operating system (OS) kernel and a multitude of basic libraries and services. Each model then comes with its feature filesystems FeatureFS-X. In the example, we have four of these filesystems, FeatureFS-0 to FeatureFS-3. They contain the differences of this feature compared to the underlying filesystem. This may be additional files, removed files, or even altered files. For any given model, a stack can then be built that includes the base filesystem and a series of feature filesystems that are overlayed in order to provide the actual final boot system. The TPM decides, based on the model number, which features to unlock, i.e.,

Unified

FeatureFS-2 Data Object

FeatureFS-2

FeatureFS-2

Model-No.: 1101b unseal the respective feature key which was used to encrypt the feature filesystem to decrypt it. The unlocking of individual features during runtime configuration is illustrated by the example shown in Fig. 2. The model number is used to denote a specific combination of encrypted feature filesystems for a model of the product line. In the example, the model number has a length of 4 bits to be able to encode the four different feature filesystems. The binary model number of 0101 b will enable the feature filesystems FeatureFS-0 and FeatureFS-2 to be loaded, since the respective bits were set within the model number's feature bitmask. The figure shows the unlocking of FeatureFS-2. As mentioned above, FeatureFS-2 is encrypted using FeatureFS-2-Key. This key is encrypted using the TPM-resident ImportTargetKey and stored together with the Policy: 0100 b in an integrity-protected Sealed Key BLOB. The integrity of the BLOB can be verified using also the ImportTargetKey. The BLOB and the encrypted FeatureFS-2 form the FeatureFS-2 Data Object. In step 1, the TPM imports the sealed key blob, decrypts the FeatureFS-2-Key, and checks the integrity of the key BLOB. The TPM verifies the policy in step 2, by checking that the third bit from the right of the policy 0100 b equals 1 (since it was also set to 1 in the model number 1101 b ). If this is true, the decrypted FeatureFS-2-Key is unsealed and transfered to the host CPU (step 3), which uses it to decrypt and mount FeatureFS-2 as part of the overlay mount (step 4).

In the example, the entire model number was used to encode the used features. It is also possible to define certain parts of the model number for encoding the used features. The remaining parts can be used for other purposes, e.g., to encode the color of the casing. In principle, the modeling of the model number can be arbitrary complex to realize certain policies (cf. Section 5.2).

Related Work

Secure Runtime Product Lines

The work in this paper extends the idea and concept of compile-time firmware product lines based upon unified software repositories to run-time firmware prod-uct lines based upon unified firmware images. The most prominent example for compile-time firmware product lines are the Yocto [START_REF] Flanagan | The Yocto Project[END_REF], OpenEmbedded [7], and BitBake [START_REF] Lauer | Building embedded linux distributions with bitbake and openembedded[END_REF] projects. The BitBake project provides the build-chain and environment for a compile-time firmware product line. OpenEmbedded and Yocto provide the core and application level software recipes to build a multitude of firmware images for a multitude of devices. The Docker project [START_REF] Docker | [END_REF] performs some form of packaging-time product lines by using overlay filesystems in their images similarly to our approach in order to stack feature filesystems. We use the same concept but for device boot of the basic operating system and additionally preventing activation and decryption of any unauthorized feature layer.

Another closely related case of product lines are so-called (feature oriented) software product lines, e.g., [START_REF] Apel | Feature-Oriented Software Product Lines[END_REF]. A lot of research has been conducted on software product lines [START_REF] Clements | Software product lines[END_REF][START_REF] Atkinson | Component-based product line development: the kobra approach[END_REF][START_REF] Gomaa | Designing Software Product Lines with UML[END_REF][START_REF] Van Gurp | On the notion of variability in software product lines[END_REF] and even their security [START_REF] Bodden | Spl lift: statically analyzing software product lines in minutes instead of years[END_REF], practical implementations exist and given the inclusion in mainstream build systems, such as autotools [START_REF]GNU: Autoconf[END_REF], they are at the core of modern software engineering. The presented approach, just as the Yocto and OpenEmbedded projects, facilitate these capabilities and use them for realizing firmware product lines.

Other related technologies that are designed with a closely related focus are called feature activation. This term refers to the activation of features on devices (similar to the presented approach), but based on additional fees payed by the device owner. Though much research has been conducted on securing feature activation [START_REF] Schramm | Secure feature activation[END_REF] and many more patents were filed, such as [START_REF] Ishii | SIM-based automatic feature activation for mobile phones[END_REF][START_REF] Fountian | Secure feature activation (Aug 25 2003)[END_REF], these works have focused on the secure transfer of activation codes; i.e., on providing the evidence for an activated feature into the device. The actual securing of the feature-relevant programs on the device were to the best of the authors knowledge not yet solved. Also note that feature activation is not the focus of the presented approach and would require a rework of the model number deployment process (cf. Section 5.2).

Finally, it is known that many firmwares today are already partially selfreconfiguring upon startup due to their model by activating or deactivating certain software services. However, the security of these features remains yet to be solved, and a plausible approach is presented in this paper.

Overlay Filesystems

Overlay filesystems combine multiple filesystems into one single virtual filesystem and directories with equal paths are merged to one path. A typical application is the combination of read only devices (e.g., a CD) with writable devices, where all changes in the read only filesystem are stored on the writable device. This example use case could be realized under Windows with the Unified Write Filter [START_REF]Overlay for Unified Write Filter (UWF)[END_REF]. For Linux the overlay filesystems AUFS [START_REF] Junjiro | Advanced multi layered unification Filesystem AUFS[END_REF] and OverlayFS [START_REF] Brown | Overlay Filesystem[END_REF] are available. AUFS is a reimplementation of UnionFS [START_REF] Unionfs | A Stackable Unification File System[END_REF] the first available implementation of an overlay filesystem for Linux. UnionFS is also available for Free BSD and Net BSD. AUFS was the first device driver used in Docker [START_REF] Docker | [END_REF] to layer Docker images and is very stable. OverlayFS is included in the mainline kernel and is potentially faster than AUFS. Despite this fact, we used AUFS in our prototypical implementation to present our concept since the structuring of the data was more simple, and AUFS did match better the requirements for the integration of encrypted SquashFS [START_REF] Squashfs | [END_REF] read only filesystems into the virtual overlay filesystem.

TPM 2.0

The second iteration of the Trusted Platform Module (TPM), namely the TPM 2.0 Library Specification [START_REF]Trusted Computing Group: Trusted Platform Module Library Specification[END_REF] has been released by the Trusted Computing Group (TCG) in October 2014. It provides a catalog of functionalities that can be used to build TPMs for different platforms. Accompanying the TPM specifications, the TCG has developed the specification of a TPM Software Stack (TSS) 2.0 for this new generation of TPMs. It consists of multiple Application Programming Interfaces (APIs) for different application scenarios [START_REF]Trusted Computing Group: TSS System Level API and TPM Command Transmission Interface Specification[END_REF][START_REF]Trusted Computing Group: TSS Feature API Specification[END_REF].

Difference of TPM 2.0 to TPM 1.2 Compared with TPM 1.2, TPM 2.0 is a complete rewrite. Many of the new features were not compatible with the data type and function layout of TPM 1.2. The new features of TPM 2.0 in comparison to TPM 1.2 include:

-Cryptographic Agility: placeholders for cryptographic algorithms, e.g. RSA, ECC, AES, SHA1, and SHA256 (cf. TCG Algorithm Registry [START_REF]Trusted Computing Group: Algorithm Registry[END_REF]). -Support of Symmetric Algorithms: AES and HMACs.

-Enhanced Authorization: TPM 1.2 provided only limited authorization mechanisms: SHA1 hashes of passwords and binding a single set of PCR values for key use and sealing. TPM 2.0 included the concept of Enhanced Authorization, that allows the forming of arbitrary policy statements based on a set of policy commands. This provides a high flexibility requiring multiple factors to be fulfilled but also to allow different paths for policy fulfillments. -Non-Volatile Memory: With TPM 2.0 the capabilities of the TPM's integrated non-volatile memory (NV-RAM) were enhanced. They can now be used as counters, bitmaps, and even extended PCRs. -Flexibility: the TPM can be realized as dedicated hardware chip but also in software, e.g., as a firmware TPM or software protected by a Trusted Execution Environment (TEE). In addition, TPM profiles can be defined to specify required functionalities of the TPM and TSS. -Many more enhancement were made. A lot of those are outline in [START_REF] Challener | A Practical Guide to TPM 2.0: Using the Trusted Platform Module in the New Age of Security[END_REF].

TPM 2.0 Features In the following, those TPM 2.0 features and command relevant for the proposed solution are briefly introduced.

-TPM Sealed Objects The TPM 2.0 can seal data. The purpose of sealing is to encrypt data with the TPM and to ensure that only this TPM can unseal the data again. In order to unseal the data, an authentication secret can be provided or a policy session that follows the scheme for Enhanced Authorization can be used. The commands used for working with sealed objects are TPM2 Create, TPM2 Import, and TPM2 Unseal.

-TPM2 Create This command is used to create all kinds of objects for the TPM. This includes sealed object as well as keys usable as import targets.

During creation, a usage policy can be provided that restricts usage of the created object. -TPM2 Import In addition to the local creation of objects inside the TPM, the TPM2 Import command further allows the external creation and importing of all kinds of objects, including keys and sealed objects. The creation of such an import blob is denoted as create Import. -TPM2 Unseal In order to retrieve the content of an encrypted, sealed object, the TPM2 Unseal command can be used. If the object was created or imported with a certain usage policy, this policy needs to be fulfilled for usage. This is done using so-called policy sessions. -TPM2 EvictControl Since the TPM only has limited persistent internal memory, objects are usually stored externally, encrypted with a TPMresident key. Any object can be made persistent inside the TPM on request by the owner. The TPM2 EvictControl command is used to store an object persistently in the TPM or to delete an object from persistent storage. -TPM NV Storage A TPM comes with an internal non-volatile memory.

This memory can be used to make keys of the TPM persistent but can also be allocated by applications. Classes of NV-Indices are Extendable NV-Indices, NV-Counters, and BitMasks. The latter can be used to individually set bits of an NV index's or to test bits within Enhanced Authorization policies. -TPM2 NV DefineSpace The TPM2 NV DefineSpace command is used to define an NV index. Depending on the assigned index number, the NV index is either part of the user-owned (storage hierarchy) or of the platform-/OEM-owned (platform hierarchy) areas of the TPM. For the sake of this paper, only OEM-owned indices are used. -TPM2 NV Read / TPM2 NV Write The TPM2 NV Read / TPM2 -NV Write command is used to read / write data to a TPM NV index. -Enhanced Authorization With Enhanced Authorization, any object that requires authorization can either be authorized using a secret value assigned during creation (similar to TPM 1.2) or using a policy scheme. Enhanced Authorization consists of a set of policy elements that are each represented via a TPM command. Currently, eighteen different policy elements exist that can be concatenated to achieve a logical and in arbitrary order and unlimited number. Two of these policy elements -PolicyOr and PolicyAuthorize -act as logical or. Due to implementation requirements, policy statements are, however, neither commutative nor distributive. Once defined they need to be used in the exact same order. In this paper, we use the following notation: P olicy abc := P olicyX 1 () ∧ P olicyX 2 () ∧ . . . P olicyX n () where P olicy abc is the "name" for this policy, such that it can be referred to from other places and P olicyX i () describes the n concatenated TPM2 Policy commands that are required to fulfill this policy. -TPM2 StartAuthSession In order to fulfill any authorization policy, the application needs to start a policy session using the TPM2 StartAuthSession command. Then the actual policy statements are subsequently satisfied by invoking the corresponding TPM commands. -TPM2 PolicyNV The PolicyNV element provides the possibility to include NV-indices in the evaluation of a policy. Amongst other operations, it can be used to test whether a certain bit is set or clear within the value of a specified NV-index: P olicy abc := P olicyN V (N V index, operation, value).

For the operation of testing where the third bit 0x0004 is set in the NV index N V abc the following statement can be used: P olicy abc := P olicyN V (N V abc , BIT SET, 0x0004). This policy will only succeed, if the equation value&0x0004 == 0x0004 evaluates to true. -TPM2 PolicyNVWritten This policy statement evaluates to true, if a given NV index has not been written to before. -sim PolicyXYZ In order to precalculate so-called policy digests -the representation of a policy used during creation -certain calculations need to be performed. To refer to these calculations, the notion of sim PolicyXYZ is used, e.g. sim PolicyNV.

Concept

Our concept for implementing Secure Runtime Firmware Product Lines consists of three parts: (1) configuration of the device during production, (2) creation of the firmware image, and (3) booting a model-specific firmware.

Device Production

During device production, two steps need to be taken. A key must be deployed to the device, that is used for importing the sealed key blobs, and the model type number must be stored inside the device's TPM.

Model Number

The model number is stored inside the NV-storage of the TPM and can be read by anybody but cannot be altered. The number will subsequently be used to test whether a certain software feature shall be decrypted and activated at boot time for the given device. It is even possible to store the model number as part of the serial number, since the TPM-operations also allow the testing of only parts of a number stored in NV memory. The purpose of the TPM2 PolicyNVWritten is to disallow subsequent writes by anybody to the model number NV index. Only as long as the NV index has not been written, can it be written. This also enables partial pre-production of products, where for example the board is assembled and fit into a chassis and the TPM is partially pre-provisioned but the model number is not yet set.

ImportTargetKey

The anchor for the decryption operations during boot is the ImportTargetKey. This key needs to be deployed to all devices of a product line. It is stored persistently inside the TPM for the lifetime of the device. This key is imported into the TPM and stored persistently using the TPM2 EvictControl command. When booting a firmware, the keys used for each of the features are imported underneath this key before being unsealed for actual usage during firmware decryption and activation.

Firmware Creation

Two additional steps are required for building a firmware image: the product line elements must be created by means of an overlay filesystem and the filesystems must be encrypted with a sealed TPM key bound to the corresponding model number bit. The process involving the TPM can be realized as follows: firmware = createBaseImage() for fs=overlay 1 to overlay N do tmpfs = createFeatureLayer() fs.bitmask = createFeatureBitmask() key = TPM2 GenRandom() fs.data = encrypt(key, tmpfs) policyDigest = sim PolicyNV(modelIdx, fs.bitmask, BITSET) fs.seal = create Import(importTargetKey, featureKey, policyDigest) firmware.add(fs) end for release(firmware) Filesystem Creation The firmware for Secure Runtime Firmware Product Lines needs to be constructed in a specific way. For this example, we assume to have a base firmware image that is common to all models of the given product line. Note though that even different base images can be provisioned, this requires more space in the resulting firmware image. For the sake of explanation, we consider the construction of a firmware image for two models ModelA and ModelB with two mutually exclusive features FeatureA and FeatureB.

A base image is constructed as file image on the build PC. For a Linux system, this would include things such as libc, base-tools, init-system, etc. Next, a second (empty) image file is created and mounted as overlay to the base image. Then the software for FeatureA is installed into the overlay filesystem. This step can also include the rewriting or even the deletion of files. Some overlay filesystems represent deletion as entries to the 0-inode for example. When unmounting the filesystem, the differences from base image to ModelA are stored inside the FeatureA filesystem. Now, a second file image can be created for FeatureB and the process of overlay mounting and installation can be repeated.

The approach can be further generalized by, e.g., mounting the images for base, FeatureA, and FeatureC versus base, FeatureB, and FeatureC if models differ for example in some intermediate layer, but not in the highest layer.

Filesystem Encryption For each of the feature filesystem layers, a bitmask is created regarding which bits inside the model number represent the activation of the corresponding feature. For example, any model number with bit 0 set (i.e., uneven numbers) will include the filesystem for FeatureA. With this information, a corresponding TPM2 PolicyNV statement can be constructed that represents the test for this bit inside the model number NV index. It can also test for multiple bits or even the complete model number. This depends on the architecture for assignment of features to model numbers. The result of the policy statement creation is a policyDigest, i.e., a hash value that represents this policy.

Then a symmetric key is created that is used for encrypting the feature filesystem image. This key is then embedded within an import blob for the target TPM. This import blob is of type keyedHash, which means that it can be unsealed on the target TPM. It includes the key for the filesystem and the policyDigest that restricts the unsealing of the key to those devices that have a model number corresponding to the policy's requirements. Finally, this import blob is encrypted using the ImportTargetKey as decryption key.

The bitmask, the encrypted key seal blob for TPM import, and the encrypted filesystem are then provided with the firmware image as a package FeatureFS-X Data BLOB. Note that the order of mounting the overlay images plays an important role, especially if file alterations or removals exist. This can be represented by naming of the files that contain the feature packages (if they are stored as files inside the firmware image) or by the order in which they are stored, if e.g., a partition table is used, where each package is contained inside its own partition.

Booting a Model-specific Firmware

During firmware boot, the specific firmware for the given model of the product line is unlocked and mounted. This process uses the following algorithm: current = mount(basefs) modelNo = TPM2 NV Read(modelIdx) for fs=overlay 1 to overlay N do if fs.bitmask == modelNo & fs.bitmask then seal = TPM2 Import(importKeyHandle, fs.seal) pSess = TPM2 StartAuthSession(PolicySession) TPM2 PolicyNV(modelIdx, fs.bitmask, BITSET, pSess) key = TPM2 Unseal(seal, pSess) overlay = decrypt(key, fs.data) current = overmount(current, overlay) end if end for current = overmount(current, localdatafs, localdata-directory) current = overmount(current, tmpfs, runtime-directory) chroot and boot(current) Basic Preparations During boot, the first step is to perform some basic operations. During this step, the basefs image is mounted and the model number is read from the TPM. This reading of the model number is not restricted in any way and can be performed by any running software. Only writing is restricted to the vendors production step.

Feature Loop The loader will loop over all features that are provided within the unified firmware image and test for each of these, whether they are activated for the given model number. Those that are not active will be skipped. For all activated features, the loader will import the sealed feature key into the TPM under the ImportTargetKey. Then it will provide a policy session that proofs to the TPM that the policy for this sealed feature key is fulfilled by the model number stored inside the TPM. Then it will request the unsealing of the feature key from the TPM, based on the policy session that proofs the correctness of this attempt. With the unsealed feature key, the loader can decrypt the feature filesystem and mount it on top over the currently mounted system -either over the basefs or over the stack of basefs and previously mounted feature overlays.

Local Configuration and Runtime Data Before switching into the final stack of overlay filesystems, the loader mounts two final filesystems. The runtime overlay is a temporary filesystem held only in RAM for the current boot cycle. This is necessary for the firmware in order to create sockets for local IPC connections, storing process identifiers, or to create temporary files for locking to schedule access to certain resources. The configuration overlay is an additional filesystem that contains local configuration data of the device. The reason for performing an overlay mount for this filesystem instead of a regular mount is that the feature filesystems can provide default configurations within their images. Thus, only changed configuration files are actually stored on local storage.

Discussion

Security

To upgrade his device to a higher-level model, an user / attacker can try the following attacks.

Attacking the TPM The attacker can try to read out the feature keys of the TPM. The secrecy of the feature keys depends directly on the secrecy of the ImportTargetKey stored inside the TPM. An extraction of this key is unlikely if a hardware TPM certified by Common Criteria (usually using EAL4+) targeting the TCG's defined Protection Profile for TPMs is used. To further mitigate the impact of a successful key extraction from the TPM, the vendor could also rotate the import key with every production batch. This will, however, require the vendor to provide import-blobs of the sealed feature keys for all of these rotated import keys. In order to compensate for the latter, the vendor can instead choose to deploy an additional intermediate key together with the firmware blobs. In this approach, every production batch would have its own import target key. Each firmware version would then include a specific intermediate import key that is prepared for importing under all import target keys. The sealed feature keys would then be encrypted for import under the intermediate keys. Given a realization with n import target keys, i.e., production batches, and m sealed feature keys, this would mean that each firmware blob includes one (unique) intermediate key that is packaged n times for the different import target keys and m sealed feature keys that are encrypted for the intermediate import key. This is a significant simplification compared to the n • m sealed feature key that would be required without an intermediate import key.

Attacking the unsealed feature keys To decrypt and mount a feature filesystem, the required feature key is decrypted by the TPM and transferred to the host CPU. An attacker could sniff on the transmission. This threat can be mitigated either by physically securing the bus between TPM and main CPU or by using the TPM protocols built-in encryption capabilities. For this, the boot-code of the device could include the public portion of the import key and use this to encrypt a salt value during session establishment. Attacks against the host CPU are not addressed by the presented approach. This includes attacks against the OS kernel or even cold boot attacks. To address the latter, mechanisms such as full memory encryption could be applied [START_REF] Henson | Memory encryption: A survey of existing techniques[END_REF].

Attacking a feature-rich model An attacker could attack a feature-rich model and try to extract an unencrypted firmware image and inject it into a low-feature device. This attack would require access to the raw RAM during runtime via a software exploit. To cope with potentially unknown vulnerabilities, appropriate mechanisms for secure code update should be applied [START_REF] Fuchs | Advanced remote firmware upgrades using TPM 2[END_REF].

Manipulation of the model number An attacker could try to change the model number to a number of a device with more features. The integrity of the model number depends on the inability of the user to write to the model number NV index. This needs to be ensured by disallowing TPM2 UndefineSpace and TPM2 UndefineSpaceSpecial with Platform-Authorization, which is supposed to be under vendor-control anyways. In order to mitigate attack potential even further, the vendor can set TPM2 NV WriteLock on model number explicitly on each boot.

Extensions

Refurbishment of Devices In many environments with device product lines, there exists the necessity to refurbish devices that are e.g. produced but never delivered. This can occur due to canceling of orders or because a certain hardware feature is defect that is required for a certain version of the device. In such scenarios, the vendor will refurbish the device to a new model by exchanging the chassis or a model number sticker on the chassis and reconfigure the firmware on the device to the new device type.

In order to support this process with the presented scheme, the policy for the model number NV index on the device can be set to a policy that allows the vendor (and only the vendor) to perform write operations on this index. Such a case can be achieve using a TPM2 PolicySigned. This policy requires an external entity to sign a challenge from the TPM in order to perform a certain operation.

Model Number Attestation Many devices nowadays are provided with the inclusion of additional services, such as cloud integration. This may, however, be a premium feature that is only activated for premium devices. The presented scheme of storing the model number inside the TPM supports such scenarios using the TPM2 NV Certify command. Using this command, the vendor's cloud service can send a challenge to the device and the TPM will certify that the device has a given model number.

Model Numbering Schemes

The presented approach uses a very simplistic scheme for activation of feature filesystem for a given model number by querying whether certain bits in the model number are set. In addition, it is possible to extend these schemes further using a combination of AND and OR in the policy statements. For example, it is possible to require a (set of) bits to be zero using the TPM2 PolicyNV with the operation TPM EO BITCLEAR. These policies can then be extended using the TPM2 PolicyOR to enable a certain feature filesystem for other bit combinations as well.

Implementation

We implemented our concept on an Intel NUC D34010WYK equipped with a TPM 2.0 implementation running Ubuntu 16.04 with kernel version 4.4. An Apache and a Samba server were used as product line element (PLE) examples. For accessing the TPM, a TSS implementation of the TPM 2.0 System API was used together with accompanying bash tools for rapid prototyping [START_REF]Software Platform for TPM 2.0[END_REF].

In the device production phase, the storage root key (SRK) of the TPM is generated, and the model number is written to the NV-Storage. The firmware creation need to construct the overlay filesystems. For this purpose, we used the AUFS [START_REF] Junjiro | Advanced multi layered unification Filesystem AUFS[END_REF]. For every product line, an encrypted SquashFS filesystem [START_REF] Squashfs | [END_REF] is created for overlay mounting. This filesystem is encrypted using dm-crypt [START_REF]dm-crypt: Linux kernel device-mapper crypto target[END_REF] container files. Dm-crypt is a Linux module used for transparent disk encryption. The AES encryption keys of the encrypted SquashFS filesystem is encrypted with a private asymmetric key. The created TPM object is protected by a policy testing the flag corresponding to the PLEin the TPM's NV model number.

For booting a model-specific firmware, the mounting of these filesystems is integrated into the boot process by using initramfs which make necessary preparations before switching to the systemd init process. A shell script for the creation of the overly filesystem is added to the bottom stage of initramfs. Scripts in this stage are executed before procfs and sysfs are moved to the real rootfs and execution is turned over to the init binary of the rootfs. The command 'mount -t aufs -o br=/r/tmps=rw:/r/02_apache:/r/ none /r/chr/' mounts the overlay filesystem with a temporary top filesystem /r/tmps, the mounted Apache Squash filesystem /r/02_apache, and the Ubuntu base system root directory /r to the mount point /r/chr. This overlay is finally mounted over the root filesystem /r/tmps and the init process is started to boot the system. Since the top filesystem of the current overlay system is a temporary filesystem, all file changes of the running system will be temporary. In this example, only the Apache SquashFS is mounted because the flag for enabling the Samba container was not set. Only the key for the encrypted Apache SquashFS file system could be unsealed because the corresponding flag was set. The booted system then produces the same state as during the firmware creation after the installation of the apache packages. This also includes correct configurations, since no overrides are provided via a local configuration overlay.

A first performance analysis showed only a negligible delay in the boot process introduced by using or concept for runtime firmware product lines.

Conclusion and Future Work

In this paper, we propose an approach for secure runtime firmware product lines. Unified firmware images can be provisioned to a whole series of products while preventing unauthorized activation of features that belong to a different model instance. Using the features of TPM 2.0 Enhanced Authorization, Sealing, and Importing we show that this scheme can be implemented by using CotS hardware. We also present an implementation, to show the feasibility of this approach and its integration with a Linux-based system. Future work includes the extension of the presented approach to include unified images for hardware product lines, similar to the OpenEmbedded's Board Support Packages and the tight integration with the build process of unified firmware images as well as a thorough performance evaluation using different embedded platforms.

  Fig. 1. General Idea

Acknowledgment

The work presented in this paper has been partly funded by the German Federal Ministry of Education and Research (BMBF) under the project "SURF".


Joseph Hallett

David Aspinall

Capturing Policies for BYOD

BYOD policies are informally specified using natural language. We show how the SP4BYOD language can help reduce ambiguity in 5 BYOD policies and link the specification of a BYOD policy to its implementation. Using a formalisation of the 5 policies written in SP4BYOD, we make comparisons between them, and explore the delegation relationships within them. We identify that whilst policy acknowledgement is a key part of all 5 policies, this is not managed by existing MDM tools.

Introduction

Employees bring their own devices to work. In the past employees might have had a dedicated company device. Today around 70% of companies have a BYOD scheme [START_REF] Schulze | BYOD & Mobile Security[END_REF]. In some fields, 85% of staff use their personal devices to look up work-sensitive information [START_REF] Patel | A UK perspective on smartphone use amongst doctors within the surgical profession[END_REF]. Controlling employee's devices is a challenge for IT departments. Failure to manage devices can lead to employees accidentally leaking confidential information. Unfortunately companies have limited control over the devices inside their networks if they do not own them.

One solution to controlling devices is requiring users follow BYOD policies. A BYOD policy takes the form of a user agreement, written in natural language, which describes how devices should be used and configured. Various guides are available for companies wishing to implement a policy from governments, standards bodies, and organizations seeking to advise [START_REF] Guerin | Security Policy for the use of handheld devices in corporate environments[END_REF][START_REF] Souppaya | Guidelines for Managing and Securing Mobile Devices in the Enterprise: NIST Special Publication 800-124 Revision 1[END_REF][START_REF] Cesg | BYOD Guidance: Good Technology[END_REF]. On top of user agreements, companies may also use Mobile Device Management (MDM) software which can help enforce policies. MDM software can configure a device's security settings, and add security APIs, helping enforce some aspects of the policies. But the use of MDM software does not guarantee compliance. One survey from a leading MDM vendor found over 50% of companies using their MDM software still had devices that did not comply with the policy [START_REF]Q4 Mobile Security and Risk Review[END_REF]. Reasons for noncompliance included out-of-date MDM configurations that hadn't been updated, and employees tampering with the MDM software.

BYOD policies are becoming more intricate. Prior work has looked at developing MDM software to enforce some aspects [START_REF] Costantino | Towards enforcing on-the-fly policies in BYOD environments[END_REF][START_REF] Martinelli | Enhancing Android Permission Through Usage Control: A BYOD Use-case[END_REF][START_REF] Armando | Enabling BYOD through secure meta-market[END_REF]. The MDM encoding of a policy is only part of the problem, however. BYOD policies are specified informally using natural language, and they contain more than just access control decisions. They describe trust relationships inside the company between IT departments, users, and HR, who each may be delegated to provide rules and make decisions. Policies contain rules that require employees to acknowledge risks, and regulations. An antivirus or MDM program may be used to implement part of the policy. But it is the policy that specifies which software to use and when. There is no automatic way to check how the policy has been implemented and by what.

Companies lack visibility as to how well they implement their policies. When considering what tools a company may use Morrow notes "particularly with the BYOD trend IT professionals do not know if anti-virus software is installed or if it's current" [START_REF] Morrow | BYOD security challenges: control and protect your most sensitive data[END_REF]. Even when devices can implement policies correctly, it is hard to configure devices that are not owned by the company [START_REF] Tokuyoshi | The security implications of BYOD[END_REF]. Our work aims to address these problems directly: by using formal languages we can link the policy to the implementation.

To describe the BYOD policies we present SP4BYOD: a formal language for linking policies to the tools used to implement them, and distributing decisions to relevant parties. Using a formalization of five BYOD policies written using SP4BYOD we identify different idioms and common delegation patterns present in BYOD policies. Our formalizations pick out the common concerns and trust relationships in these policies. We look at what decisions and trust relationships are used in BYOD policies. We identify BYOD idioms that capture frequently seen decisions in BYOD policies. These give a guide for where future work implementing MDM tools should focus their efforts to cover more aspects of policies.

SP4BYOD is not designed to replace existing static and dynamic analysis and enforcement tools. A company might use multiple tools, app stores, or contractual agreements with employees to enforce their policies. We aim to help clarify the meaning of ambiguous natural language policy documents, and provide a rigorous means for following them. A company can use any MDM tool, curated app store or user agreement to enforce their policy. SP4BYOD links the specification of the policy to its implementation, showing exactly how a policy is implemented and giving a rigorous means to enforce it.

We show how SP4BYOD can be used to encode policies and describe precisely the different trust relationships. SP4BYOD is an instantiation of the SecPAL authorization language [START_REF] Becker | SecPAL: Design and semantics of a decentralized authorization language[END_REF] for mobile device policies and implemented atop of AppPAL [START_REF] Hallett | AppPAL for Android[END_REF], which adds mobile device specific predicates to SecPAL, for example, capturing app permissions. SecPAL is also a useful tool for describing other policies surrounding mobile ecosystems [START_REF] Hallett | Specifying BYOD Policies with Authorization Logic[END_REF]. Our SP4BYOD implementation can be easily extended to support new types of policies. It also gives us access to tooling we have developed to check SP4BYOD policies for completeness and redundant statements. For this work additional tooling was developed to help visualise policies and describe their contents. This was helpful for making comparisons between policies and checking our formalisation for mistakes.

In summary, our work makes the following contributions: -We present a formalisation of five different BYOD policies in SP4BYOD: a new instantiation of SecPAL for describing BYOD policies (Section 2).

-Using our formalisation of the policies we make comparisons between the different policies. Unlike previous work which looks at individual policies [START_REF] Armando | Developing a NATO BYOD security policy[END_REF], our work looks at policies across a variety of domains (Section 4). -We identify that delegation and acknowledgements are an important aspect of BYOD policies that current MDM software does not look at (Section 6).

1 [START_REF] Armando | Bring Your Own Device, Securely[END_REF]. Their tool allows companies to distribute apps through a secure app store [START_REF] Armando | Enabling BYOD through secure meta-market[END_REF]. The store ensures apps meet policies through a combination of static analysis and app rewriting with dynamic enforcement. Their policies are low level, based on ConSpec [START_REF] Aktug | ConSpec A Formal Language for Policy Specification[END_REF], allowing checks based on Dalvik VM's state. Using their tool, they implemented parts of a NATO Communications and Information Agency policy relating to personal networks and data management [START_REF] Armando | Developing a NATO BYOD security policy[END_REF]. Their work shows how the app-specific sections of a BYOD policy can be check and enforced using tools. They did not look at where the checks or policies come from, however.

An SP4BYOD policy might use BYODroid to ensure that parts of a policy are enforced (as well as other tools for other parts). Using SP4BYOD, we can distribute policies by sharing signed statements from different principals. We can delegate to other marketplaces to decide if an app meets different parts of policies. We can even create new stores by composing their policies and using multiple store's statements about the apps. Distributing checks like this is useful when using some static analysis tools which can take a long time to run (e.g. TaintDroid [START_REF] Enck | TaintDroid: An Information-Flow Tracking System for Realtime Privacy Monitoring on Smartphones[END_REF]).

Tools, such as Dr. Android and Mr. Hyde [START_REF] Jeon | Hide: fine-grained permissions in android applications[END_REF] and Aurasium [START_REF] Xu | Aurasium: Practical Policy Enforcement for Android Applications[END_REF], have suggested app wrapping (where an app is recompiled to use guarded APIs) as a possible way to enforce policies. App rewriting has the advantage that the device's underlying OS needn't be modified as the apps are changed at the source code level. However app wrapping alone without additional analysis is insufficient to enforce policies effectively [START_REF] Hao | On the effectiveness of API-level access control using bytecode rewriting in Android[END_REF].

Our approach taken with SP4BYOD is similar to work on safety cases. A safety case is an argument made to say a system is acceptably safe to be used in a given scenario. Industrial safety cases are often described in natural language, which can be ambiguous and unclear. Goal Structuring Notation (GSN) [START_REF] Kelly | The goal structuring notationa safety argument notation[END_REF] is one approach to make the safety cases explicit. It is a graphical formal notation that lets engineers argue that a system is safe by linking safety goals to the arguments made for a system's safety. Similarly, work developing a formal language for specifying how medical staff should collaborate in a healthcare scenario [START_REF] Papapanagiotou | Formal verification of collaboration patterns in healthcare[END_REF] again helps clarify how roles are filled in a medical context on the basis of staff and different healthcare providers.

It is interesting to examine how leading [START_REF] Smith | Magic Quadrant for Enterprise Mobility Management Suites[END_REF] MDM tools such as IBM's MaaS360, or Blackberry Enterprise Services (BES), enforce BYOD policies. These tools support enforcing and checking compliance policies. They do not, however, use policy languages to specify policies; rather they provide a limited number of checkboxes that admins can tweak (an excerpt of a policy from MaaS360 is shown in Figure 1). These tools allow administrators to configure a device's settings and provision the devices with company apps. Some support app wrapping, which enables them to encrypt app data locally, use a VPN within the app, or prevent apps not being used when the device isn't compliant. But because the policies are inflexible and tightly coupled to the device's OS, intervention by an administrator is often required. Whilst MDM software is good at configuring devices, selecting which policies to apply is typically a manual process performed by an administrator. Removing blacklisted apps is a common feature, but the selection process of which apps to remove is manual. As mobile devices have become more common in the workplace, BYOD policies have been written to help control them. Part of their policies are prescriptive: if you configure your device in this way, you will mitigate that threat. The policies contain more than just configuration, however. Consider this rule taken from the Security Policy for the use of handheld devices in corporate environments by SANS [START_REF] Guerin | Security Policy for the use of handheld devices in corporate environments[END_REF].

SANS: Digital camera embedded on handheld devices might be disabled in restricted environments, according to COMPANY NAME risk analysis. In sensitive facilities, information can be stolen using pictures and possibly sent using MMS or E-mail services.

In high-security facilities such as R&D labs or design manufacturers, camera MUST be disabled. Furthermore, MMS messages should be disabled as well, to prevent malicious users from sending proprietary pictures.

A company could use an MDM program to enforce this. Some MDM tools can use geofencing to apply a policies in the area around a lab. Techniques like this would implement the recommendation within the rule, but the rule itself contains more than just configuration. It talks of restricted environments decided by company risk analysis. How is this communicated to the device? Does it access the list of restricted environments once from a server, are they fixed or can a device decide them for itself? Can it judge using a policy if a location is restricted? The rule also gives a security objective: prevent malicious users from sending proprietary pictures. The guidelines are given, however, for the case of a legitimate user using MMS or email. It may not be sufficient to stop a sufficiently motivated malicious user.

Our approach does not try to enforce the policy by checking the app's code for programming errors. Rather we act as a "glue-layer" between the high-level policy and the tools and trust relationships used to implement them. We capture the goals of the policy rules so that the delegations of trust, tools implementing the policy and their configuration are made explicit. This gives us greater clarity as to which tool is being trusted to implement what policy. It allows us to see who is being trusted to make which decisions, and use automatic-tools to uncover problematic aspects of the policy [START_REF] Hallett | Specifying BYOD Policies with Authorization Logic[END_REF]. Continuing with the example above, we can encode this in SP4BYOD as: D mustDisableIn(Location, 'camera'), D mustDisableIn(Location, 'mms'), Location isHighSecurityFacility.

After checking the policy we generate a proof tree that shows how the policy was satisfied. These proof trees not only show how the policy was followed but also provide an audit trail. In a company decisions may be delegated to different departments. Auditors can see what happened when things go wrong. They know who made what decision, and whether they made it through following policy rules or as a stated fact.

Instantiating SecPAL

SecPAL was developed as a distributed access control language [START_REF] Becker | SecPAL: Design and semantics of a decentralized authorization language[END_REF]. It is designed to be have a clear readable syntax, and intuitive semantics. It is also designed to be extensible, which makes it ideal for extending to create new languages. All SecPAL statements are said by an explicit authority. The authority can say a fact (that something is described by a predicate), a delegation (that someone else can-say a fact), or a role assignment (that something can-act-as something else). This statement optionally contain conditional facts, and constraints that must be satisfied before the authority will say the statement.

To create SP4BYOD we instantiate SecPAL with four kinds of facts common in BYOD policies: can, has, is and must. Like other SecPAL-based instantiations [START_REF] Becker | A Framework for Privacy Preferences and Data-Handling Policies[END_REF][START_REF] Aziz | SecPAL4DSA: A Policy Language for Specifying Data Sharing Agreements[END_REF] we extend the syntax of facts to support these constructs.

Fact Meaning subject canAction

The subject is permitted to perform the action. subject hasAction The subject has performed the action. subject isType The subject is a member of the type. subject mustAction The subject must perform the action.

Facts of the must-kind represent obligations, actions to complete if a particular scenario presents itself. For these facts, we add a rule to check we perform the obligation. This rule should be checked periodically to ensure compliance. Our implementation contains tooling to generate these rules automatically, by parsing the policy.

speaker says subject hasSatisfiedObligation Action if subject must Action , subject has Action .

Facts using is predicates give types to variables. SP4BYOD inherits from SecPAL's (and Datalog's) safety condition that the body of a statements must reference all the variables in the head. This can lead to some boilerplate code in policies that may obscure their meaning. To simplify the policies, we add syntactic sugar for facts giving variables their type (variable isType). Variables in the head of the statement of the form Type :Variable are replaced by the variable and a condition Variable isType is added to the condition. The two statements shown below (taken from the SANS policy) are equivalent, however we feel the example on the right is easier to read.

'company' says Device canConnectToAP(X) if X isOwnedByCompany, Device isDevice, X isAP.

'company' says Device:D canConnectToAP(AP:X) if X isOwnedByCompany.

BYOD Policies

We examined 5 policies and encoded them into SP4BYOD looking for common idioms. We selected these policies as they came from a variety of domains.

-The first is the Security Policy Template: Use of Handheld Devices in a Corporate Environment, published by the SANS Institute [START_REF] Guerin | Security Policy for the use of handheld devices in corporate environments[END_REF]. This policy is a hypothetical policy published to help companies mitigate the threats to corporate assets caused by mobile devices. Companies are expected to modify the document to suit their needs. The policy is general; not specific to any particular industry, device, or country's legislation. -The second is taken from the Healthcare Information Management System Society (HiMSS) [START_REF]Mobile Security Toolkit: Sample Mobile Device User Agreement[END_REF]; a US non-profit company trying to improve healthcare through IT. The HiMSS policy is relatively short and contains concerns specific to healthcare scenarios. It is written as a contract the users agree to follow. In contrast, every other policy we looked at is written as an organisation imposing rules on users they should follow to ensure compliance. The policy is designed as a sample agreement for a system trying to manage personal mobile devices in a healthcare environment. -The third is taken from a British hospital trust [START_REF] Kennington | Mobiles Devices Policy[END_REF] and describes the BYOD scheme used in practice at the hospital. -Finally, we looked at two simpler policies from The University of Edinburgh [START_REF] Williamson | Bring Your Own Device Policy[END_REF] and a company specialising in emergency sirens [START_REF]Sample BYOD Policy[END_REF]. These policies are simpler, and shorter than the other policies we looked at comprised of much more general rules.

We summarise the policies in Table 1. Each policy contains a series of rules, which we implemented by one or more SP4BYOD statements. The policy coverage represents the number of rules that have an SP4BYOD description attached.

All five of the policies make use of acknowledgements. The use of an acknowledgements could be because enforcing that rule in a policy through technical means is undesirable. It could indicate policy authors care more that the subjects Only the NHS and SANS policies, the two most complex policies, describe when a device can install an app and what kinds of apps are installable. In both policies this expressed as a delegation to the appropriate groups to authorize an app. For example, in the SANS policy the IT-Department are responsible for deciding what apps can be installed. The NHS policy, however, is significantly more complicated. Apps have to be approved by three different groups (the IGC, the Employee's manager, and the relevant group for either clinical or business cases) before the Trust will say that an employee can install an app.

NHS: Apps for work usage must not be downloaded onto corporately issued mobile devices (even if approved on the NHS apps store) unless they have been approved through the following Trust channels: Clinical apps; at the time of writing there are no apps clinically approved by the Trust for use with patients/clients. However, if a member of staff believes that there are clinical apps or other technologies that could benefit their patients/clients, this should be discussed with the clinical lead in the first instance and ratification should be sought via the Care and Clinical Policies Group. A clinical app should not be used if it has not been approved via this group. Business apps; at the time of writing there are no business (i.e., non-clinical) apps approved by the Trust for use other than those preloaded onto the device at the point of issue. However, if a member of staff believes that there are apps or other technologies that could benefit their non-clinical work, ratification of the app must be sought via the Management of Information Group (MIG). An app should not be used if it has not been approved via this group. Following approval through Care and Clinical Policies and/or MIG, final approval will be required through Integrated Governance Committee. Use of paid apps must be agreed in advance with the device holder's line manager and there should be a demonstrable benefit.

'nhs-trust' says App isUsable if App hasMet('clinical-use-case').

'nhs-trust' says App isUsable if App hasMet('business-use-case'). 'nhs-trust' says 'cacpg' can-say App:A hasMet('clinical-use-case'). 'nhs-trust' says 'mig' can-say App:A hasMet('business-use-case'). 'nhs-trust' says App isInstallable if App hasMet('final-app-approval'), App isUsable. 'nhs-trust' says 'igc ' can-say App hasMet('final-app-approval'). 'nhs-trust' says Device canInstall(App)

if App isInstallable, App isApprovedFor(Device). 'nhs-trust' says Employee:Manager can-say App:A isApprovedFor(Device) if Manager isResponsibleFor(Device).

We might expect corporate policies to describe what apps can be installed in terms of the apps functionality. This does not appear to be the case, however.

As part of selecting the apps, an IT department or group may choose to use advanced instrumentation and policies [START_REF] Armando | Enabling BYOD through secure meta-market[END_REF]. Alternatively, they may manually chose apps to form a curated app store as some MDM vendors allow. From the perspective of the policy, it is more important who makes the decision rather than what they chose, however.

Authorization Example

As a worked-example consider the NHS rules for finding approved apps (Section 4). Suppose an employee, Alice, wished to get an app, com.microsoft.office, installed on their device. To do so, Alice would have to convince the device that:

'nhs-trust' says ' alices -phone' canInstall('com.microsoft.office ').

Alice wishes to use the app for business so to satisfy the policy Alice must collect the following statements:

-'nhs-trust' says 'com.microsoft . office ' isInstallable.

For this, she needs a statement from the Management of Information Group that it has a business use-case. She also needs approval from the Integrated Governance Committee. 1. 'mig' says 'com.microsoft . office ' hasMet('business-use-case').

2. ' igc ' says 'com.microsoft . office ' hasMet(' final -app-approval'). -'nhs-trust' says 'com.microsoft . office ' isApprovedFor('alices-device'). To get this she needs a statement from the manager responsible for Alice's device (Bob) approving the app. 3. 'bob' says 'com.microsoft . office ' isApprovedFor('alices-device'). 4. 'nhs-trust' says 'bob' isResponsibleFor('alices-device'). -Additionally, she needs the following typing statements.

5. 'nhs-trust' says 'com.microsoft . office ' isApp.

6. 'nhs-trust' says 'bob' isEmployee.

Alice obtains the statements by contacting each of the speakers. Each may either give her the statement she needs or may give her additional rules. For example, the MIG and IGC may be happy to state their statements (after a review). When checking if the app is an App in Item 5, the NHS trust may be instead inclined to delegate further. They could reply that if the App is in the Google Play store then they are convinced it is an app. Alice would then have to obtain additional statements if she wanted to prove this statement. As with SecPAL, all statements should have a signature from their speaker proving they said the statement. Alternatively, the speaker could refuse to give the statement, either because they do not believe it to be true, or they cannot give an answer. In this case, Alice would have to look for an alternative means to prove the statement or accept that they cannot install the app.

When the statements have been collected Alice can use a SecPAL inference tool (such as AppPAL2 ) to check the policy has been satisfied. The generated proof from the tool lets auditors review how the decision was made, and verify the decision-making process.

BYOD Idioms

When examining the policies, we noticed two particular idioms in many policies: acknowledgements and delegation. We describe both idioms in greater detail, and show how they can be implemented in SP4BYOD, below. MDM tools and research have focussed so far on implementing restrictions on apps and devices [START_REF]IBM MaaS360 -Enterprise Mobility Management (EMM)[END_REF][START_REF] Armando | Formal modeling and automatic enforcement of Bring Your Own Device policies[END_REF][START_REF] Martinelli | Enhancing Android Permission Through Usage Control: A BYOD Use-case[END_REF]. Implementing these controls is a vital aspect of BYOD policies and all 5 of the policies we looked at had rules that described restrictions (Table 1). Every policy also contained rules that required employees acknowledgements, however. Only the SANS policy (which is configuration focussed) contained more rules that required restrictions than acknowledgements. All the policies contained more rules featuring delegation relationships than functionality restrictions.

Delegation and Roles within Policies. Delegation is an important part of each of the policies. Each of the policies describes through rules how separate entities may be responsible for making some decisions. These rules can be a delegation to an employee's manager to authorize a decision (as in the NHS policy). It could be to technical staff to decide what apps are part of a standard install (as in the sirens and SANS policies).

SP4BYOD requires an explicit speaker for each statement. Speakers can delegate to others by making a statement about what they can-say. When translating the policies, the author of the policy is used as the primary speaker of the policy's rule (Table 1). For the HiMSS policy, where the user states what they will do rather than the company stating what they must, the user is the primary speaker. All the policies describe multiple entities that might make statements and delegate. With SP4BYOD policies any speaker can delegate a decision to another speaker (with restrictions on re-delegation). The delegation might be to a user to acknowledge a policy, or it might be to other groups in the company who are responsible for certain decisions.

In all the policies we looked at the majority of the decisions are made by three groups of speakers: the company, the IT-department, and the users or employees. All the policies also delegate to a user (apart from HiMSS where the user is the primary speaker). The user is typically responsible for providing information, such as agreements to policies, reporting devices missing, and updating passcodes. In the Sirens, SANS and NHS policy each describe an IT-department who are delegated to make some decisions. The HiMSS policy describes an xyz-healthsystem who act similarly to an IT-department. These decisions are more varied and can overlap with the responsibilities of the company. In the NHS and SANS policies, the IT department is responsible for maintaining lists of activated devices. In the Sirens and SANS policies, the IT department maintains a list of what is installable on a device or not.

When a policy decision requires input from a third-party delegation is used. For example, an employee's manager has to authorise an app install. The SecPAL can-say statement is the basis for a delegation. We can ask the HR department to state who is someone's manager.

'company' says 'hr-department' can-say

Employee:E hasManager(Employee:M).

If we wish to delegate to someone, we can add conditionals to the can-say statement that enforces any relationship between the delegating and delegated parties.

'company' says Manager can-say Employee canInstall(App:A) if Employee hasManager(Manager).

Acknowledgement. All the policies we looked at require their subjects to be aware and acknowledge certain rules or policies, and that the company may perform certain actions. For example, the NHS and HiMSS policies state that the organisation will wipe devices remotely to protect confidential information a user loses their device. Both policies also say that employees would lose personal information if they had it on the device and the company needed to erase it. The employee is required to be aware of this, and in the case of the HiMSS policy, agree to hold the company harmless for the loss. Both the SANS and the siren-company policies use acknowledgements to link to other sets of rules that employees should follow. These policies are not further specified, and in the case of an acceptable use policy may be hard to enforce automatically. The SANS policy requires that all employees follow an email security, acceptable use, and an eCommerce-security policy. The Sirens policy expects an employee to use their devices ethically and abide by an acceptable use policy.

When there is a (usually separate) set of rules and concerns employees should be aware of acknowledgements are used. The company may not wish to enforce these separate rules automatically, however. For instance, a company may have an ethics policy that says employees should not use devices for criminal purposes. The company is not interested in, or capable of, defining what is criminal. They trust their employees to make the right decision and to be aware of the rules.

To implement these in SP4BYOD, a policy author creates two rules: the first stating their employees must have acknowledged the policy, the second delegating the acceptance of the policy to the employee themselves.

'company' says Employee:E mustAcknowledged('policy'). 'company' says Employee:E can-say E hasAcknowledged('policy').

Conclusions

We have presented SP4BYOD: an instantiation of SecPAL for BYOD policies.

Using an SP4BYOD formalization of 5 BYOD policies we have identified that whilst delegation and acknowledgement form a large part of written BYOD policies, existing BYOD tools ignore them. BYOD policies contain delegation and trust relationships that define who is responsible for making different decisions in a company. Sometimes that is administrators and technical staff deciding what to permit inside the company, and sometimes it is the user's themselves agreeing to follow a policy. Previous work has focussed on the technical staff's decisions and developing new ways to automate their decisions. Our work looks at the policies at a higher level tracking, managing and authorizing policies based on what people have said and what tools were run. SP4BYOD improves upon existing MDM tools by allowing sophisticated delegation relations and by providing a declarative language for expressing policies. The language gives greater flexibility to policy authors and allows them to write policies that depend on other policies rather than predefined settings and groups. It lets us track what users have agreed to, what their policies are, how they are specified, and how they are satisfied.

Fig. 1 .

 1 Fig. 1. Excerpt of a policy showing network settings from MaaS360.

Table 1 .

 1 Summary of the contents of each of the BYOD policies.are aware of the rules than they do for rigorous enforcement. All but the HiMSS policy have rules that include locking down a device by disabling features. All but the Edinburgh policy have rules that look at what should happen if a user loses their device. The rest have rules that require employees inform someone when something happens. Common concerns, such as these, suggest where future MDM software should focus their efforts.

		SANS	HiMSS	NHS	Edinburgh	Sirens
	Number of rules	33	15	56	20	25
	SP4BYOD statements	71	21	58	10	39
	Policy coverage	33 (100%) 14 (93%) 40 (71%)	10 (100%) 1	22 (88%)
	Rules using Acknowledgement	2	10	11	1	6
	Rules using Delegation	23	5	33	2	13
	Rules describing a restriction	18	3	8	1	5
	Principal Speaker	company	user	nhs-trust records-management department

The Edinburgh policy contains a large number of rules that whilst marked as such are in fact just descriptions of the document. All the policy rules that described restrictions or relationships were implemented in SP4BYOD.

https://github.com/apppal/libapppal

Acknowledgements were used in all the policies, but were not a part of MDM tools. A purely speculative explanation for this might be that the people using the MDM software (the IT department) do not care about the acknowledgements, and that another department (HR perhaps) are responsible for tracking what corporate policies employees have agreed to and have their own methods for dealing with that. Future work will aim to further explore how these acknowledgements are used within a company and how to manage them in a practical manner.

Related systems, such as GSN described in Subsection 1.1, use a graphical notation. Whilst SecPAL-based languages are designed to be readable, diagrams can help make authors write policies and auditors understand them. Future work will look at extending SecPAL's notation to create such diagrams and further aid readability.

Work supported by EPSRC App Guarden grant (EP/K032666/1) and the Alan Turing Institute. 'company' says 'risk-analyst' can-say Location:L isHighSecurityFacility. 'company' says Device:D mustDisableIn(Location, 'camera') if Location isHighSecurityFacility. 'company' says Device:D mustDisableIn(Location, 'mms') if Location isHighSecurityFacility.


Edoardo Serra

Jaideep Vaidya

Haritha Akella

Ashish Sharma

Evaluating the Privacy Implications of Frequent Itemset Disclosure

Keywords:

Frequent itemset mining is a fundamental data analytics task. In many cases, due to privacy concerns, only the frequent itemsets are released instead of the underlying data. However, it is not clear how to evaluate the privacy implications of the disclosure of the frequent itemsets. Towards this, in this paper, we define the k-distant-IFM-solutions problem, which aims to find k transaction datasets whose pair distance is maximized. The degree of difference between the reconstructed datasets provides a way to evaluate the privacy risk. Since the problem is NPhard, we propose a 2-approximate solution as well as faster heuristics, and evaluate them on real data.

Introduction and Related Work

Frequent itemset mining [START_REF] Agrawal | Mining association rules between sets of items in large databases[END_REF] is a crucial data mining task which has numerous applications in knowledge discovery such as recommendation, classification, etc. Many efficient implementations exist, [START_REF] Goethals | Fimi03: Workshop on frequent itemset mining implementations[END_REF], all of which assume that the underlying database is accessible to the data miner. However, often privacy concerns prohibit the direct release of data. Since frequent itemsets can serve as a good proxy for the underlying data and still enable different kinds of analysis, often they are released instead. Prior work has examined whether it is possible to find the original dataset from the frequent itemsets, defined as the Inverse frequent set mining (IFM) problem and studied from several different perspectives [START_REF] Mielikainen | On inverse frequent set mining[END_REF][START_REF] Guzzo | An effective approach to inverse frequent set mining[END_REF][START_REF] Guzzo | Solving inverse frequent itemset mining with infrequency constraints via large-scale linear programs[END_REF][START_REF] Calders | Itemset frequency satisfiability: Complexity and axiomatization[END_REF]. IFM aims to find a transaction dataset D that satisfies a given set of itemset support constraints (i.e., the support or frequency of an itemset should be contained within the specified numeric interval). Wang and Wu [START_REF] Wang | Approximate inverse frequent itemset mining: Privacy, complexity, and approximation[END_REF] also introduced the ApproSUPP problem, where they asked whether it is possible to satisfy the various support constraints in an approximate fashion and presented an ILP formulation along with heuristic strategies. Several alternative heuristics have also been proposed [START_REF] Wu | Privacy-aware market basket data set generation: An feasible approach for inverse frequent set mining[END_REF][START_REF] Ramesh | Feasible itemeset distributions in data mining: theory and application[END_REF] However, while IFM provides a measure of the degree of difficulty in inverting a set of support constraints into a dataset producing these, there is no notion of how different that dataset is from the original that needs to be protected.

In this paper, we precisely tackle this problem. We formulate a new problem called the k-distant-IFM-solutions which combines the IFM problem with elements of K-anonymity [START_REF] Samarati | Protecting respondents identities in microdata release[END_REF] and L-diversity [START_REF] Machanavajjhala | l-diversity: Privacy beyond k-anonymity[END_REF]. Specifically, the problem consists in finding k IFM solutions (transaction datasets) whose pair distance is maximized. This ensures that we have at least k different solutions to the IFM problem that are all potentially quite different. Since any of these could be the source, and are as different as possible from each other, this gives a minimum bound on the degree of privacy afforded by the frequent itemsets. We show that the problem is NP-hard, and give a 2-approximation based on the greedy strategy. However, given the complexity of the underlying problem, we also develop a heuristic based on an ILP formulation (see [START_REF] Schrijver | Theory of Linear and Integer Programming[END_REF]) that is quite efficient. Thus, our work is orthogonal to all of the prior work, since it considers the problem of finding multiple datasets meeting the given set of support constraints, and provides a better estimate of the risk of disclosure through the frequent itemsets. . Given a dataset D, the frequent itemset mining problem aims to find all of the itemsets whose frequency is greater than a given threshold.

Problem Statement

In our paper, we assume that instead of releasing the actual dataset, only a set of itemsets is released along with their frequencies due to privacy concerns. However, in this case, the problem that we study is the extent to which it is possible to retrieve the original dataset D. This is related to the Inverse Frequent itemset Mining (IFM) problem, which aims to find a dataset such that the frequencies of a set of given itemsets for that dataset are in a specific range interval. IFM is formally defined as follows:

The IFM problem Given a set of items I, two integer numbers s l , s u , a set of support constraints S of the form (I, l, u) where I is an itemset on I and l, u ∈ N with l ≤ u. The IFM problem, denoted as IF M (I, s l , s u , S), consists in finding a dataset D such that s l ≤ |D| ≤ s u and ∀(I, l, u) ∈ S : l ≤ support(l, D) ≤ u.

Given a set of support constraints S, IFM provides information about degree of difficulty of generating a dataset that produces those frequent itemsets. However, note that while the solution to IFM enables malicious users to find a dataset that also meets the same support constraints, it does not say anything about whether this is the real dataset or how different it is from the real dataset. Indeed, given a set of support constraints S, more than one dataset solution can exist for the IFM problem. While this increases uncertainty in terms of the actual dataset, it may not significantly increase privacy since all of the datasets might be quite similar, thus actually reducing privacy.

Thus, to enable evaluation of the privacy risk associated with frequent itemset disclosure, we formalize a new problem called k-distant-IFM-solutions, i.e. find k IFM solutions whose pair distance is maximized. If we can find a sufficient number of solutions that are quite different from each other, then it significantly increases the degree of uncertainty and thus privacy. We can also take into consideration the problem of finding subset of support constraints or a perturbed version that can maximize the pair distance among all of the k IFM solutions.

K-distant-IFM-solutions problem

We first define the distance between two datasets, and then formalize the actual problem. While Jaccard or Hamming distance is a good metric to measure the distance between two individual transactions, they cannot directly be used to measure the difference among the collection of transactions. In our problem, the number of duplicate transactions has a significant meaning and therefore we chose to define our own metric that extends the Hamming distance for collection of transactions. Furthermore, we use the edit distance constraint to ensure that the different datasets obtained are sufficiently apart from each other based on our distance metric. Consider a case where the dataset D 1 = {{a, b, c}, {a, b, c}, {a, b, f }} and D 2 = {{a, b, c, h}, {a, b, c, h}, {a, b, f, h}}. Since there are no transactions in common, (D 1 , D 2 ) = 6 is the maximum distance that can be obtained.However, these datasets are exactly the same except for the item h. The edit distance constraint addresses this issue.

Given two datasets D 1 and D 2 over I, we define the function dist(D 1 , D 2 ) between D 1 and D 2 as

dist(D 1 , D 2 ) = t∈T D 1 ∪T D 2 |# D1 (t) -# D2 (t)|
This distance is a metric, but we omit the proof due to lack of space. end while 8:

Algorithm 1 Greedy Algorithm

return SD; 9: end procedure

k-distant-IFM-solutions

Given a set of items I, a positive integer number k, two integer numbers s l , s u , a set of support constraints S of the following form (I, l, u) where I is an itemset on I and l, u ∈ R. The k-distant-IFM-solutions problem consists of finding a set of k datasets SD = {D 1 , . . . , D k } such that for each D ∈ SD, D is a solution of IF M (I, s l , s u , S), and the pair distance

pairDist(SD) = Dj ,Di∈SD,i>j dist(D i , D j ) is maximized. Theorem 1. The k-distant-IFM-solutions problem is NP-hard.
Since finding even one solution of IF M (I, s l , s u , S) is NP-hard (as shown in [START_REF] Calders | Itemset frequency satisfiability: Complexity and axiomatization[END_REF]), finding k solutions is also NP-hard.

Proposed Approach

We now discuss how this problem can be solved. Let us assume SOL(I, S) is the set of all datasets that are the solution of IF M (I, S).

Thus, the k-distant-IFM-solutions can be formalized as

SD * ∈ arg max SD⊆SOL(I,S),|SD|=k pairDist(SD)
For this problem, Borodin et al. [START_REF] Borodin | Max-sum diversification, monotone submodular functions and dynamic updates[END_REF] show that if the function dist is a metric, then the Greedy Algorithm (Algorithm 1) gives a 2-approximate solution. However, we still need to specify how steps 3 and 6 of Algorithm 1 will be executed, i.e. how to choose D * ∈ SOL(I, S) (for step 3) and D * ∈ arg max D∈SOL(I,S)\SD pairDist(SD ∪ D) (for step 6). Step 3 simply requires finding a solution for IFM, which is well understood. For the sake of simplicity and efficiency, we simply choose the first feasible solution instead of choosing a solution randomly. We denote the problem in Step 6 as the Maximum Distant Dataset and now show how to solve it.

Maximum Distant Dataset

The goal of maximization is to maximize the difference between the created dataset and existing datasets. Thus, we would like to find a dataset D that maximizes D ∈SD dist(D , D), which is equivalent to maximizing pairDist(SD∪D). In order to solve the Maximum Distant Dataset we provide an ILP formulation. This formulation is based on three kinds of variables:

-a real variable x t ,
|# D (t) -x t |.
Now, the formulation is as follows:

maximize D∈SD t∈T D y D t + t⊆I,t ∈T D xt (1) t⊆I,I⊆t xt ≥ l (I, l, ) ∈ S (2) t⊆I,I⊆t xt ≤ u (I, , u) ∈ S (3) t⊆I xt ≥ s l (4) t⊆I xt ≤ su (5) #D(t) -xt ≤ y D t D ∈ SD, t ∈ TD (6) -#D(t) + xt ≤ y D t D ∈ SD, t ∈ TD (7) #D(t) -xt + 2 * kt * (1 -z D t ) ≥ y D t D ∈ SD, t ∈ TD (8) -#D(t) + xt + 2 * kt * z D t ≥ y D t D ∈ SD, t ∈ TD (9)
xt ≥ 0 t ⊆ I (10)

y D t ≥ 0 D ∈ SD, t ∈ TD (11) z D t ∈ {0, 1} D ∈ SD, t ∈ TD (12)
Where, k t = min(s u , min (I, ,u)∈S,I⊆t u).

As can be seen, we have two groups of constraints. The first group of constraints from 2 to 5 defines the minimum support, the maximum support, the minimum size and the maximum size, respectively. The second group constraints from 6 to 9 contribute in modeling the absolute value |# D (t)-x t | is equal to y D t . More specifically, constraints 6 and 7 impose that |# D (t) -x t | ≤ y D t ensuring that the variable y D t is an upper bound of the absolute difference between x t and # D (t). Constraints 8 and 9 impose that only one condition between # D (t) -x t and x t -# D (t) has to be greater than or equal to y D t . Latter two constraints ensure that y D t is also the lower bound of the absolute difference between x t and # D (t). The constraints from 6 to 9, together, ensure that y D t = # D (t) -x t . However, note that only one of the constraints between 8 and 9 can be met. z D t is the decision variable activating one of these two constraings, while k D t is the smallest constant that is large enough to ensure that these constraints are met. Finally, the maximization function (expression 1) maximizes the degree of difference in support for transactions present, which exactly models the maximization of distance metric defined in 2.1.

Usually, adding more constraints to an integer linear program reduces the search space by improving the bound obtained by the linear formulation and consequently reduces the computation time. Therefore, we define additional constraints and variables imposing that the value

y D t = |# D (t)-x t | is max(# D (t), x t )- min(# D (t), x t ).
The real variables y D t,max and y D t,min model max(# D (t), x t ) and min(# D (t), x t ), respectively. The revised ILP is given below. Note that in this case, the integer variables and the constraints are polynomial in the description of SD and S, respectively. The main issue is represented by the exponential number of real variables x t due to all the possible transactions t ⊆ I. Thus, these linear programs cannot really be directly solved. However, we can use an alternative technique called the branch and price algorithm (see [START_REF] Barnhart | Branch-and-price: Column generation for solving huge integer programs[END_REF]).

#D(t) ≥ y D t,min D ∈ SD, t ∈ TD (13) xt ≥ y D t,min D ∈ SD, t ∈ TD (14) #D(t) ≤ y D t,max D ∈ SD, t ∈ TD (15) xt ≤ y D t,max D ∈ SD, t ∈ TD (16) #D(t)(1 -z D t ) ≤ y D t,min D ∈ SD, t ∈ TD (17) xt -kt * (1 -z D t ) ≤ y D t,min D ∈ SD, t ∈ TD (18) (#D(t) -kt) * z D t + kt ≥ y D t,max D ∈ SD, t ∈ TD (19) xt + kt * z D t ≥ y D t,max D ∈ SD, t ∈ TD (20) y D t,max -y D t,min = y D t D ∈ SD, t ∈ TD (21) y D t,max + y D t,min = #D(t) + xt D ∈ SD, t ∈ TD (22) y D t,min ≥ 0 D ∈ SD, t ∈ TD (23) y D t,max ≥ 0 D ∈ SD, t ∈ TD (24)
Algorithm 2 HeuristicSolver

Heuristic Solver

The branch and price algorithm is a branch and bound algorithm that at each branch solves the relaxed problem (i.e. the linear one) by using column generation techniques. Given that the number of variables is huge, column generation techniques make the problem tractable. Instead of working on the entire set of variables, the column generation technique starts with a prefixed number (in our case the variables related to all the transactions in SD) and at each iteration it generates a new variable or column (a new transaction) whose reduced cost is negative [START_REF] Calders | Itemset frequency satisfiability: Complexity and axiomatization[END_REF] [START_REF] Guzzo | An effective approach to inverse frequent set mining[END_REF]. In order to generate a new variable a new problem called price problem has to be solved. The price problem consists of finding a new column with negative reduce cost, which is strictly related to the simplex algorithm [START_REF] Schrijver | Theory of Linear and Integer Programming[END_REF] and how it works. Note that the specific price problem changes based on the underlying LP or ILP formulation. In prior work [START_REF] Guzzo | An effective approach to inverse frequent set mining[END_REF] the problem in Definition 2 has already been formalized as a linear program whose constraints are the constraints from 2 to 5. [START_REF] Guzzo | An effective approach to inverse frequent set mining[END_REF] also solves it with a column generation techniques and its price problem. In our problem we start by considering all the variables referring to all the transactions in SD. Then the new variables or columns that we have to generate are those not involved in the constraints from 6 to 22. The main idea is to use the column generation techniques to solve the relaxation formulation where all the binary variables are substituted with real variables restricted to [0, 1]. Then, use all the columns generated in the column generation algorithm to solve the ILP version. Algorithm 2 gives the details.

Price problem

The pricing problem consists in finding a new transaction different from all the previous transactions whose reduced cost is negative. It is known that the reduced cost of a column can be expressed as a linear combination of the dual variable associated to each constraint of the linear program (see [START_REF] Guzzo | Solving inverse frequent itemset mining with infrequency constraints via large-scale linear programs[END_REF]). Let dsl, dsu, dl I and du I (where (I, , ) ∈ S) be the dual variables associated to the constraints of the kinds 4, 5, 2 and 3. The reduced cost of a transaction t is rc(t) = 1 + dsl + dsu + I⊆t,(I, , )∈S (dl I + du I ). Given the set of current datasets generated SD, the set of all the different transactions present in SD is defined as tr(SD) = D∈SD T D . Now, we show an integer linear program solving the price problem. A generic transaction is a set of items then we can represent this transaction by using |I| binary variable {q i |i ∈ I} s.t. if the item i is contained in t then q i = 1 or q i = 0 otherwise. In order to model the reduced cost function, it is essential to know which of the itemset in S are contained in the new transaction. Therefore, we define a set of binary variables {h I |(I, , ) ∈ S} s.t. if the itemset I (with (I, , ) ∈ S) is contained in the new transaction then h I = 1 or h I = 0 otherwise.

The objective function represents the reduced cost of the new transaction. The first two constraints 26 and 27, impose that whether the transaction represented by the set of variables {q i |i ∈ I} contains an itemset I, the variable h I is equal to 1 or 0 otherwise. The third constraint 28 imposes that the edit distance between each transaction in tr(SD) and the new one has to be greater than or equal to the constant minED. minED can be one if we only want that the current transaction should be different by each other, but can be more than one to enforce that all the transactions in all the K datasets generated are very different. This parameter is very important in order to produce datasets different not only in terms of number of duplicates, but also in terms of transaction structure. The last constraint 29 imposes that the transaction is not an empty set. Thus, the following integer linear program finds a new transaction s.t. its reduced cost is minimized. Note that after solving this ILP program we have to check if the reduced cost is negative, and only continue to iterate if so. Otherwise, the heuristic solver stops because there does not exist any transaction with negative reduced cost.

minimize 1 + dsl + dsu + (I, , )∈S hI • (dlI + duI ) (25) hI ≤ qi (I, , ) ∈ S, i ∈ I (26) i∈I qi ≤ |I| -1 + hI (I, , ) ∈ S (27) i∈t (1 -qi) + i∈I\t qi ≥ minED t ∈ tr(SD) (28) i∈I qi ≥ 1 (29) qi ∈ {0, 1} i ∈ I (30) hI ∈ {0, 1} (I, , ) ∈ S (31)

Experimental Evaluation

We now discuss the experimental evaluation. Three datasets -2 real datasets (BMS-Webview-1, BMS-Webview-2) and a synthetic one (T10I4D100K) -were used to conduct experiments. The dataset parameters are given in Table 1. Each instance of our problem is represented by several parameters: sizemax (s u ), sizemin (s l ), set of items (I), set of support constraints S (at different levels of support), support values (ρ), k (number of different datasets to be generated), edit distance (minED). Sizemax and Sizemin were obtained for each dataset by adding and subtracting 10000 from the size of the original dataset, respectively (as noted in Table 1). minED was set to 1, 10, 20, 30, and K was varied from 2 to 11 (inclusive).

EXECUTION TIME (SEC)

ρ = 0. 3% ρ = 0. 4% ρ = 0. 5% ρ = 0. 6% ρ = 0. 7% ρ = 0. 8% ρ = 0. 9% ρ = 1. 0% (

EXECUTION TIME (SEC)

ρ = 0. 8% ρ = 0. 9% ρ = 1. 0% (
In order to generate the support constraints, of the form (I, l, u), we compute the set of the frequent itemsets from each datasets where the minimum support value δ was varied in the the range 0.2%, 0.3%, 0.4%..., 0.9%, 1%. The lower and the upper bound threshold for each frequent itemset I were obtained by using the following formulas l = support(I, D) * (1-∆) and u = support(I, D) * (1+∆)

where the interval threshold (∆) was set to values 0.0, 0.05, 0.1, 0.15, 0.2 . Thus, when ∆ = 0.0, we have that l = u = support(I, D).

All experiments were carried out on machines with CentOS7 (x86-64) Operating System, 2 Xeon Processors (E5-2620 v3 @ 2.40GHz), and 256GB RAM. We report the execution time as well as the pairDist calculated for each dataset.

Varying ∆: We first observe the impact of varying itemset interval threshold ∆ on execution time. k (the number of datasets to create) has been varied from 2-11. It was observed that the execution time was almost constant with varying interval threshold ∆ values in the interval {0.0, 0.05, 0.1, 0.15, 0.2} for all the three datasets except for ∆ = 0.0 for which execution time increased. Figures 1a through 1c represent the impact of k-anonymity values and interval threshold values on execution time for the three datasets. The results show that as we increase the value of delta, the flexibility allowed to the solver also increases and it quickly finds a feasible solution.

Varying support threshold values: We next observe the impact of varying k along with varying support threshold values on the execution time for solving a k-distant-IFM-solution. Figures 2a through 2c show the impact of varying k on execution time. It can be noted that while the time required is different for the three datasets for the different support threshold values, it does not change much with respect to k. For BMS Webview-2 and T10I4D100K datasets with varying ρ%, similar trend is observed. In [START_REF] Guzzo | An effective approach to inverse frequent set mining[END_REF] (which models IFM with linear programs), increasing ρ% decreases the execution time. However, for integer linear formulations with more constraints, search space is decreased and it is easier to find a solution. Therefore, increase in ρ%, increases the execution time.

Due to the significant computational resources required and the large number of experiments to be carried out, we were only able to carry out experiments for a few values of support for BMS Webview2 dataset. But we did check to make sure that the overall behavior is the same. For T10I4D100K dataset, lower values of support lead to a huge number of frequent itemsets. Therefore, we limited the experiments to higher values of support. Also, the behavior of execution time with respect to k is clear even when k is limited to 11, which was sufficient reason not to go beyond 11 for k as these operations are computationally expensive. Varying edit-distance values: We next observe the impact of varying editdistance values in the range [START_REF] Agrawal | Mining association rules between sets of items in large databases[END_REF][START_REF] Ramesh | Feasible itemeset distributions in data mining: theory and application[END_REF]20,30]. Figures 3a -3c show the impact on execution time for the three datasets. We can generally observe that time does not significantly change by varying the edit distance. Pairwise average distance varying k, ρ and ∆: Finally, we observe the effect of varying k, ρ and ∆ on the pairwise distance. Firstly, for varying support constraints ρ and k, figures 4a through 4c show the impact of k w.r.t. distance/((k * (k -1))/2) values for the three datasets. Here, no specific trend can be observed. However, if we consider that our approach is based on 2approximation algorithm, these trends can be considered constant within an approximation range. Similarly, if we consider the case where we vary ρ, it can be observed that as the support increases, the average distance decreases and Secondly, for varying interval threshold ∆, figures 4d through 4f show the impact of k values w.r.t. distance/((k * (k -1))/2) for the three datasets. We can observe that as interval ∆ decreases, the average distance also decreases. Essentially, increasing the support interval size for each itemset increases the uncertainty of the itemset distribution and thus decreases the privacy risk. Additionally, note that in fig 4c andfig 4f, there is a peak in the plots between k = 2 and k = 3. This is because Algorithm 1 in line 3 initialize the SD with an arbitrary transaction database which is not chosen in a way that would maximize the distance of the future transaction database candidates.

EXECUTION TIME (SEC)

ρ = 0. 8% ρ = 0. 9% ρ = 1. 0% (

Conclusion

In this paper we define the K-distant-IFM-solutions problem, that enables evaluation of the frequent itemset disclosure risk and propose a solution for it. The experimental evaluation shows that the proposed approach is effective. In our future work, we plan to develop methodologies that are able to perturb the support of the itemsets disclosed in order to minimize the disclosure risk. In addition, we plan to extend these techniques to work with sequence mining as well -where we consider sequences rather than itemsets.

Let 2 Example 1 .

 21 I be a set of items. An itemset I is a subset of I. A transaction Dataset D is a pair (T D , # D ), where T D is a set of transactions (i.e. itemsets) contained in D and # D : 2 I → N is a function assigning to each transaction a number of duplicates such that if t ∈ T D then # D (t) > 0, otherwise # D (t) Let I = {a, b, c}. Following is an example of a transaction database where # D (t) = 0 for each transaction t that is not present in T D and # D (t) > 0 for transactions that are present in T D . Given an itemset I, the support of I w.r.t. D is support(I, D) = t∈T D ,I⊆t # D (t) and its frequency is f requency(I, D) = support(I,D) |D|

1 :

 1 procedure greedyAlgorithm(I, S) 2: SD = ∅; 3: Choose D * ∈ SOL(I, S) 4: while (|SD| ≤ k) do 5: SD = SD ∪ {D * }; 6: Choose D * ∈ arg max D∈SOL(I,S)\SD pairDist(SD ∪ D); 7:

1 Fig. 1 :

 11 Fig. 1: Varying k and interval threshold ∆

  a) BMS WebView1: ∆ = 0.05, MinED = 1

Fig. 2 :

 2 Fig. 2: Varying Support Threshold

Fig. 3 :

 3 Fig. 3: Varying edit-distance for different ∆ and k

10 Fig. 4 :

 104 Fig. 4: Average Distance w.r.t varying ρ and ∆

  for each possible transaction t ⊆ I, modeling the number of duplicates #(t) for each transaction t in the dataset that we have to generate (we relax the assumption that number of duplicates is an integer number); Effectively, the variable x t gives the support count of the transaction t in the newly created dataset.a real variable y D t , for each D ∈ SD and t ∈ T D , modeling the values |# D (t)x t |; Note that for all transactions t present in the existing datasets, |#D(t)x t | gives the absolute difference in support for such transactions in each dataset D. For the transactions t that are not present in the existing datasets, x t directly gives the support of such transactions in the new dataset.a binary variable z D

t , for each D ∈ SD and t ∈ T D , that is used to emulate the absolute value

  procedure HeuristicSolver((SD, S, s l , su)) 2:Generate integer linear program P according SD, S, s l and su where the set of variables with prefix x is only equal to {xt|D ∈ SD, t ∈ TD};

	3:	Relax in P the binary constraints the variables with prefix z;
	4:	Solve the program P ;
	5:	Find a new transaction t (if it exists) by solving the price problem;
	6:	while (t exists) do
	7:	Add the variable xt in P ;
	8:	Solve the program P ;
	9:	Find a new transaction t (if it exists) by solving the price problem;
	10:	end while
	11:	Add in P the binary constraints on the the variables with prefix z;
	12:	Solve the program P ;
	13:	Obtain from the solution of P the dataset D;
	14:	return D;
	15: end procedure

1:

Table 1 :

 1 Dataset Description

	Dataset Name Real Dataset Distinct Avg. trans. Max trans. s l	su
		Size	Items	Size	Size
	BMS WebView1	59602	497	2.5	267	49602 69602
	BMS WebView2	77512	3340	4.6	161	67512 87512
	T10I4D100K	100000	870	10	300	90000 110000

This work was supported by Idaho Global Entrepreneurial Mission (IGEM) program Grant 131G106011 (Precision Ag -Increasing Crop), the National Science Foundation Grant CNS-1422501 and the National Institutes of Health Award R01GM118574. The content is solely the responsibility of the authors and does not necessarily represent the official views of the agencies funding the research.