Antitza Dantcheva
email: antitza.dantcheva@inria.fr

Francois Bremond
email: francois.bremond@inria.fr

Piotr Bilinski
email: piotrb@robots.ox.ac.uk

Show me your face and I will tell you your height, weight and body mass index

Body height, weight, as well as the associated and composite body mass index (BMI) are human attributes of pertinence due to their use in a number of applications including surveillance, re-identification, image retrieval systems, as well as healthcare. Previous work on automated estimation of height, weight and BMI has predominantly focused on 2D and 3D fullbody images and videos. Little attention has been given to the use of face for estimating such traits. Motivated by the above, we here explore the possibility of estimating height, weight and BMI from single-shot facial images by proposing a regression method based on the 50-layers ResNet-architecture. In addition, we present a novel dataset consisting of 1026 subjects and show results, which suggest that facial images contain discriminatory information pertaining to height, weight and BMI, comparable to that of body-images and videos. Finally, we perform a genderbased analysis of the prediction of height, weight and BMI.

I. INTRODUCTION

The human face exhibits information pertaining to identity, a person's disposition, demeanor, as well as to attributes such as gender, age and ethnicity. From the perspective of biometrics, emphasis has predominantly been placed on facial recognition. More recently attributes or soft biometrics [START_REF] Jain | Soft biometric traits for personal recognition systems[END_REF], [START_REF] Dantcheva | What else does your biometric data reveal? a survey on soft biometrics[END_REF], [START_REF] Nixon | On soft biometrics[END_REF], [START_REF] Dantcheva | Gender estimation based on smiledynamics[END_REF], [START_REF] Chen | Impact of facial cosmetics on automatic gender and age estimation algorithms[END_REF] such as gender, age, height and weight have gained popularity due to their semantic interpretation, i.e., they can provide a description that can be readily understood by humans; for example the description "young, female, tall". Limited attention has been given to the connection between the human face and body characteristics such as body height and weight and even less so on the automatic extraction of such.

Estimating body height, weight and the associated BMI is warranted for several reasons. Firstly height and weight are attributes frequently used in surveillance, forensics, as well as re-identification applications and image retrieval systems [START_REF] Bekios-Calfa | Robust gender recognition by exploiting facial attributes dependencies[END_REF]. Secondly, height and weight are primary and obvious attributes used by humans to verbally describe a person often used in police reports, unlike traditional biometrics which may be insufficient, as this was argued, for example, by Klontz and Jain [START_REF] Klontz | A case study on unconstrained facial recognition using the boston marathon bombings suspects[END_REF] in the case of the 2013 Boston bombings. Thirdly, body weight and height have been proposed as soft biometric traits in automated biometric systems [START_REF] Dantcheva | Bag of soft biometrics for person identification[END_REF]. Fourthly, weight is a pertinent indicator for health and excessive weight has been associated to obesity, diabetes, and cardiovascular diseases. In this context, the presented method contributes to the current trend of image-based automated self diagnostic. Finally, this work can promote research conducted in psychology related to human metrology [START_REF] Coetzee | Deciphering faces: Quantifiable visual cues to weight[END_REF], [START_REF] Pham | Body mass index and facial cues in sasang typology for young and elderly persons[END_REF], [START_REF] Adjeroh | Predictability and correlation in human metrology[END_REF].

A. Contributions

Motivated by the above, in this work we (a) propose a new ResNet-based method for estimating body weight, height and BMI from the face. In order to conduct this study, we (b) assemble a new dataset of facial images, annotated for gender, body height, weight and BMI. In addition, (c) we provide an analysis on the impact of gender on the above estimation.

The rest of the paper is organized as follow. In Section II we review work on methods used for the estimation of height, weight and BMI. Section III introduces the proposed facebased height, weight and BMI estimation algorithm. Datasets and experimental protocol are described in Section IV. Section V presents experiments validating the effectiveness of the proposed method and a discussion thereof. Finally, Section VI concludes the paper.

II. RELATED WORK

To the best of our knowledge, the only work related to automated face-based estimation of BMI is a study by Wen and Guo [START_REF] Wen | A computational approach to body mass index prediction from face images[END_REF], based on the MORPH-II dataset, which obtained mean absolute errors (MAEs) for BMI in the range from 2.65 -4.29 for different ethnic categories. The study explored handcrafted features for BMI-estimation and specifically in the method the face was detected, normalized, and an active shape model was fitted, based on which, geometry and ratio features were extracted (cheekbone to jaw width, width to upper facial height ratio, perimeter to area ratio, eye size, lower face to face height ratio, face width to lower face height ratio and mean of eyebrow height), normalized and finally subjected to support vector regression. We note that the BMI-annotation of MORPH-II has not been made public.

Body weight and BMI have received an increased attention in the recent years. This relates to different trends that have appeared, such as for example the fact that more than twothirds of U.S. adults are now overweight or obese [START_REF] Yates | Secular trends in the diagnosis and treatment of obesity among us adults in the primary care setting[END_REF], and the fact that obesity -which is now recognized as a disease by the American Medical Association 1 -accounts for nearly one out of every 10 American deaths. Specifically an increased body weight and thus BMI, is associated with many health problems such as diabetes, heart disease, certain cancers , strokes, osteoarthritis and gallstones, all of which cost the United States 223 billion per year2 . These motivate the use of automated extraction of body weight and of BMI -computed from body weight and body height as:

BM I = weight[kg] height 2 [m 2 ] = weight[lb] • 703 height 2 [in 2 ] , (1)
which further has the advantage of being contactless, low-cost, unobtrusive, and unconstrained 3 . Body weight has been estimated from manually measured body-anthropometric data [START_REF] Velardo | Weight estimation from visual body appearance[END_REF] by constructing a weight prediction metric using multiple regression analysis. Related experiments on the NHANES dataset 4 -which contains data of 28,000 subjects -showed that weight could be estimated in 93% of the test data with an error of less than 10%. In addition, an automated and Kinect based weight estimation [START_REF] Velardo | Building the space scale or how to weigh a person with no gravity[END_REF] from full-body shots obtained weight estimation error of 4% in a small dataset of 15 subjects. Furthermore a related work for weight estimation by Labati et al. [START_REF] Labati | Weight estimation from frame sequences using computational intelligence techniques[END_REF] studied frame sequences representing walking subjects. Under specific video acquisition from calibrated cameras, body height, body volume (estimated by ellipses passing through the silhouettes), body shape and walking direction were extracted, to train a neural network towards body weight estimation. The mean errors ranged from -2.38 kg to 0.02 kg, and they corresponded to a private dataset of 20 subjects.

Human estimation of body weight from face and body [START_REF] Bloomfield | Accuracy of weight and height estimation in an intensive care unit: Implications for clinical practice and research[END_REF] has shown to be rather imprecise, with 47% of estimates at least 10% different and 19% of estimates at least 20% different from the measured values. The majority of height estimates were within 10% of the measured values. Similar results were obtained by a study by Coe et al. [START_REF] Coe | The accuracy of visual estimation of weight and height in pre-operative supine patients[END_REF], where four observers estimated the weight and height of 38 patients who were lying covered on operating theatre trolleys. In addition, drug dosages and infusion rates in adults are usually based on body weight, as are nutrition prescriptions [START_REF] Morgan | Lean body mass as a predictor of drug dosage: Implications for drug therapy[END_REF], [START_REF] Jolliet | Enteral nutrition in intensive care patients: A practical approach[END_REF]. Nomograms, such as the Cockcroft-Gault and the Harris-Benedict formulas, as well as intensive care unit (ICU) scoring systems, such as SOFA (Sequential Organ Failure Assessment), rely on knowledge of the patients weight [START_REF] Cockcroft | Prediction of creatinine clearance from serum creatinine[END_REF], [START_REF] Simpson | Parenteral vs. enteral nutrition in the critically ill patient: A metaanalysis of trials using the intention to treat principle[END_REF], [START_REF] Vincent | The sofa sepsis-related organ failure assessment score to describe organ dysfunction failure[END_REF].

On a different, but related note concerning correlation of face and body metrology the work by Adjeroh et al. [START_REF] Adjeroh | Predictability and correlation in human metrology[END_REF] used the manual 1D-measurements of the 3D CAESAR database 5to show a high degree of correlation clusters between face and body measurements. Utilizing the existing correlation, gender could be estimated with a success rate of 100% (this corresponded to 44 measurements), and body weight could be estimated with a success rate of 92.5%. Furthermore Criminisi et al. [START_REF] Criminisi | Single view metrology[END_REF] computed 3D affine measurements from single perspective views, where affine scene structure could be determined from the image, without knowledge of the camera's internal calibration (e.g., focal length), nor of the explicit human pose.

Height is also required for calculations of ideal body weight or adjusted body weight [START_REF] Carney | Current concepts in nutritional assessment[END_REF], [START_REF] Bl | Dosing of medications in morbidly obese patients in the intensive care unit setting[END_REF], and height or weight is used to calculate and communicate ventilator settings [START_REF] Eichacker | Meta-analysis of acute lung injury and acute respiratory distress syndrome trials testing low tidal volumes[END_REF].

Both weight and height are required to estimate body surface area, cardiac index and body mass index [START_REF] Carney | Current concepts in nutritional assessment[END_REF], [START_REF] Gibson | The importance of metabolic rate and the folly of body surface area calculations[END_REF]. In addition, application of many commonly used clinical guidelines and evidence-based practices require the knowledge of height and weight. We here note that while generally, patients can be weighed and measured or questioned, in some cases (i.e., elderly trauma patients or intensive care patients) measuring or questioning is not an option due to decreasing mental ability, as well as immobility or unconsciousness. Finally, we note that the failure to obtain and record weight and height has been highlighted in the National Confidential Enquiry into Peri-operative Deaths (NCEPOD) [START_REF] Callum | National confidential enquiry into perioperative deaths[END_REF] reports, concluding that accurate estimation or measurement of height and weight of critically ill patients is a pertinent prereposite to optimum clinical care.

A. Convolutional Neural Networks

Deep Convolutional Neural Networks have significantly advanced attribute recognition, where existing architectures such as AlexNet [START_REF] Liu | Deep learning face attributes in the wild[END_REF], VGG [START_REF] He | A jointly learned deep architecture for facial attribute analysis and face detection in the wild[END_REF] and Inception [START_REF] Sarfraz | Deep viewsensitive pedestrian attribute inference in an end-to-end model[END_REF] have been employed and adapted. One finding has been that when pretraining with massive face images, high-level hidden neurons automatically learn semantic concepts and that such concepts are significantly enriched after fine-tuning with attribute tags. Further, a deep model pre-trained for face recognition, implicitly learns attributes.

III. PROPOSED APPROACH

Motivated by the above, we propose here a method for face-based estimation of height, weight and BMI based on the ResNet-50 architecture.

We pose the problems of height, weight and BMI estimation as 3 separate regression pattern classification problems. We employ face detection prior to the ResNet as an attention mechanicsm. While deep neural networks (DNNs) tackle challenging settings of attributes in the wild that encompass complex face variations such as poses, lightings, and occlusions reasonably well and generally no face detection is required, we ensure by detecting the face, that no body information is considered in our study and hence we analyze the face-based height, weight and BMI estimation.

In what follows, we proceed to describe briefly the preprocessing step of face detection and the employed ResNetarchitecture.

A. Face Detection

There exist a large number of face detection algorithms, based on a large number of features and implementations. For our employed datasets the classic Viola-Jones algorithm [START_REF] Viola | Robust real-time face detection[END_REF] performed very well (100% correctly detected faces) and we hence incorporate it in the proposed algorithm.

We resize the detected faces to 256×256, and provide these as input of ResNet.

B. Residual Neural Networks

We employ in this work a residual network, the 50-layer ResNet [START_REF] He | Deep residual learning for image recognition[END_REF] Residual blocks with identity mapping can be represented by the following

x l+1 = x l + F(x l , W l ), (2)
where x l+1 and x l are input and output of the l-th unit in the network, F is a residual function and W l are parameters of the block. The characteristic of residual networks lies in their architecture based on sequentially stacked residual blocks. We use basic blocks with two consecutive 3 × 3 convolutions with batch normalization and ReLU preceding convolution. We use the original conv -BN -ReLU for order of batch normalization, activation and convolution in residual blocks.

C. Implementation Details

We replaced the initial 1000-d fc of ResNet with a 1-d fc and then Smooth L1 Loss in order to cater regression.

Experimental Setup: We train our network end-to-end with the classical back-propagation algorithm using a single NVIDIA GeForce GTX TITAN X with 12 GB memory. We implement our approach in the Caffe deep learning framework [START_REF] Jia | Caffe: Convolutional architecture for fast feature embedding[END_REF].

A 224×224 crop is randomly sampled from each image or its horizontal flip, with the per-pixel mean subtracted following the work of He et al. [START_REF] He | Deep residual learning for image recognition[END_REF]. In addition, we initialize the weights using those from the ResNet-50 model [START_REF] He | Deep residual learning for image recognition[END_REF], which were pre-trained on the ImageNet Large-Scale Visual Recognition Challenge (ILSVRC) 2014 [START_REF] Russakovsky | Imagenet large scale visual recognition challenge[END_REF] (1000-class ImageNet classification task), and then we fine-tune in turn the finer strides on the V IP attribute dataset. We use the stochastic gradient descent (SGD) algorithm with a mini-batch size of 16. The learning rate starts from 1e -5 and then we use the "inv" learning rate decay policy, which is implemented as follows:

base lr * (1 + gamma * iter) (-power) , ( 3
)
where gamma is 0.001 and power is 0.75. We use a weight decay of 0.0005 and a momentum of 0.9. The models are trained for up to 400, 000 iterations.

IV. EXPERIMENTS

A. Dataset

For this study, we assembled a dataset, which we refer to as the V IP attribute dataset, consisting of 1026 subjects, specifically 513 female and 513 male celebrities (mainly actors, singers and athletes) collected from the WWW. The images are mainly frontal images. Co-variates include illumination, expression, image quality and resolution. Further challenging are beautification (photoshop) of the images, as well as the presence of makeup, plastic surgery, beard and mustache. We obtained annotations related to the subjects' body weight and height available on websites such as www.celebheights.com, www.howtallis.org and celebsize.com, and proceeded to calculate the associated BMI. Figure 2 illustrates example images of the V IP attribute dataset. Table I reports the statistics of gender, height, weight and BMI associated to the dataset. The related histograms are depicted in Figure 3. We note that the annotation might not be fully accurate, e.g., weight fluctuations throughout time or inaccurate self-report. Images from the V IP attribute dataset are available in the authors webpage: http://www. antitza.com/VIP attribute-dataset.html.

ρ Y,Z = cov(Y, Z) σ Y σ Z = E(Y Y )(ZZ) σ Y σ Z , (4)
where σ Y and σ Z are the respective standard deviations for Y and Z. The coefficient ranges between -1 and 1, with the two extreme points being obtained when the variables are maximally linearly related. We compute the correlation coefficients between each pair of {gender height, weight, gender}, see Table II. We observe naturally a large correlation between BMI and weight, lesser with height which is due to the fact that ρ Y Z represents a linear correlation between Y and Z. Interestingly body weight and body height have intrinsically a large correlation. In agreement with previous studies [START_REF] Cao | Can facial metrology predict gender?[END_REF], height, weight and hence BMI are strongly correlated with gender.

V. RESULTS

In this section, we evaluate the performance of the proposed height, weight and BMI estimating methods on the V IP attribute dataset. As accuracy measures we report the Mean Absolute Error (MAE) and the Pearson's correlation coefficient ρ for each estimation related to height, weight and BMI. We compute the MAEs as the average of the absolute errors between the estimated height, weight and BMI and the respective ground truth.

M AE = 1 N N k=1 | bk -b k |,
where b k is the ground truth for image k, hatb k is the associated estimated value (height, weight or BMI) and N is the total number of test images. MAEs has been often used as performance measure in age estimation [START_REF] Dantcheva | What else does your biometric data reveal? a survey on soft biometrics[END_REF].

Higher errors generally related to atypical cases such as the cases of 'under weight' and 'obese' subjects, as well as to 'short' and 'very tall' subjects, due to the limited number of training samples.

A. Height

As presented in Table III, when estimating height from faces, MAEs [m] in the range of 0.077 + 0.005 were obtained. Given the statistics shown in Table I, this corresponds to < 5% of the female, male and hence overall average height, comparatively similar to human estimation [START_REF] Bloomfield | Accuracy of weight and height estimation in an intensive care unit: Implications for clinical practice and research[END_REF], which reportedly lay within the the < 10% range. The related ρs range between 0.57 and 0.60. Notable is that while MAEs pertained to females and males are smaller than the MAE of all subjects combined, the related correlation rates are higher for the latter. Overall we cannot observe a gender-bias in height-estimation.

B. Weight

We report the regression accuracy related to weight in Table IV. We observe MAEs between 8.06kg (females) and 8.51kg (all subjects). The lower MAE of females is intuitive, since females have generally a lower body weight (see Table I and Figure 3). It constitutes though about 14% of the mean weight. This is marginally larger than the weight estimation, given several precise body-measurements [START_REF] Velardo | Weight estimation from visual body appearance[END_REF], which constituted in reportedly less than 10% in 93% of the cases. Kinectaided weight estimation based on body images has shown though a significantly better performance [START_REF] Velardo | Building the space scale or how to weigh a person with no gravity[END_REF], [START_REF] Labati | Weight estimation from frame sequences using computational intelligence techniques[END_REF]. The associated human accuracy is though rather imprecise too, with 47% of estimates at least 10% different and 19% of estimates at least 20% different from the measured values [START_REF] Bloomfield | Accuracy of weight and height estimation in an intensive care unit: Implications for clinical practice and research[END_REF]. On the other hand for females we have a very high correlation rate of ρ > 0.78.

We envision, that specifically what contributes to the error in weight estimation are factors including: imprecise weight annotation, due to weight-fluctuations in time, as well as which might have been purposely augmented in favor of the subjects, face alterations such as (facial) plastic surgery, facial makeup and beautification of images (e.g., by Photoshop).

C. BMI

We report the BMI-regression accuracy in Table V. The MAEs related to BMI are in the range of 2.3 + 0.06, which is relatively small, given the absolute range of BMI, predominantly between 15 -35, illustrated in Figure 3 (c). We outperform the results of Wen and Guo et al. [START_REF] Wen | A computational approach to body mass index prediction from face images[END_REF], which were 2.65-4.29. The fluctuations between female, male and overall estimation with respect to MAEs and ρ are minimal, which indicates that BMI-estimation is not gender-biased.

VI. SUMMARY

This paper presented a novel approach for estimating height, weight and BMI from single-shot facial images, based on ResNet-50. Experiments conducted on a new dataset, which we have made publicly available, resulted in promising correlation accuracies of up to ρ = 0.78 for female weight estimation and mean absolute errors of 2.3 for female BMIestimation. We did not observe a significant gender-bias in estimating height, weight and BMI. However, more work is necessary in this regard. Future work will involve the additional study of age and ethnicity in order to improve utilization of facial appearance for height, weight and BMI estimation. The height, weight and BMI estimator was motivated by the current need for self-diagnostic tools for remote healthcare, as well as for soft biometrics categorization in security applications.

  architecture. While training deep neural networks bared challenges such as exploding / vanishing gradients and degradation, residual links met the challenge and have shown to surpass other techniques such as initialization strategies, better optimizers, skip connections, knowledge transfer, as well as layer-wise training enabling training of deeper neural networks. The incorporated residual connections have been inherently necessary for training very deep convolutional networks. ResNets have significantly progressed accuracy of object classification, object detection and segmentation, while improving the training speed.

Fig. 1 .

 1 Fig. 1. 50-layer ResNet architecture used in this work.

Fig. 2 .

 2 Fig. 2. Examples of six subjects in the V IP attribute dataset assembled by the authors.

  (σ = 0.09) 1.85 (σ = 0.14) Weight [cm] 58.34 (σ = 11.02) 86.93 (σ = 21.00) Body mass index 20.87 (σ = 3.71) 25.21 (σ = 3.57) B. Correlation between height, weight, BMI and gender Given two vectors Y = y 1 , y 2 , ..., y n and Z = z 1 , z 2 , ..., z n the Pearson correlation coefficient is computed as

Fig. 3 .

 3 Fig. 3. Histograms of (a) height, (b) weight and (c) BMI in the V IP attribute dataset assembled by the authors.

TABLE I CHARACTERISTICS

 I OF V IP attribute dataset. MEAN AND STANDARD DEVIATIONS (σ) PERTAINED TO WEIGHT, HEIGHT AND BODY MASS INDEX FOR FEMALES AND MALES.

TABLE II PEARSON

 II 'S CORRELATION COEFFICIENT FOR GENDER, HEIGHT, WEIGHT AND BMI IN THE V IP attribute DATASET.

		gender height weight	BMI
	gender	1	0.59	0.65	0.51
	height	0.59	1	0.79	0.27
	weight	0.65	0.79	1	0.78
	BMI	0.51	0.27	0.78	1

TABLE III RESULTS

 III OF HEIGHT ESTIMATION [M]. ABBREVIATIONS USED: MAE: MEAN ABSOLUTE ERROR, ρ: PEARSON'S CORRELATION COEFFICIENT.

		Male	Female	All
	MAE [m]	0.077	0.078	0.082
	ρ	0.57	0.57	0.60

TABLE IV RESULTS

 IV OF WEIGHT ESTIMATION [KG]. ABBREVIATIONS USED: MAE: MEAN ABSOLUTE ERROR, ρ: PEARSON'S CORRELATION COEFFICIENT.

		Male	Female	All
	MAE [kg]	8.25	8.06	8.51
	ρ	0.76	0.78	0.75

TABLE V RESULTS

 V OF BMI ESTIMATION. ABBREVIATIONS USED: MAE: MEAN ABSOLUTE ERROR, ρ: PEARSON'S CORRELATION COEFFICIENT.

		Male	Female	All
	MAE	2.32	2.30	2.36
	ρ	0.55	0.55	0.55

www.ama-assn.org/go/obesity

http://www.health.harvard.edu/newsletters/harvard mens health watch/ 2012/February

Extracting BMI or body weight offers also advantages, even in forensics, as these measures can be sensed at a distance and are relatively distinctive and permanent

http://www.cdc.gov/nchs/nhanes.htm

http://www.hec.afrl.af.mil/cardlab/CAESAR/index.html


Keywords: Aiborne LiDAR, coast line, dune foot, erosion, Observatoire de la côte Aquitaine

Airborne LiDAR derived geomorphological indicators to analyse pluriannual evolution of sandy beach systems at regional scale.

Under an apparent uniformity, the 230 kilometers of the Aquitanian sandy coast presents many nuances/differences in terms of geomorphological evolutions at event, seasonal, annual and pluriannual time scales. The Aquitanian Coast Observatory (OCA), through various measurement protocols, tracks and characterizes these evolutions at regional scale, focusing on sedimentary sub-cells and in view of hydro-meteorological forcing. As part of a partnership with the National Geographic Institute (IGN), the OCA has and shares LiDAR data covering the entire Aquitanian coast for the years 2011, 2014, 2016 and 2017. The surveys are carried out in autumn, during low spring tides, allowing the maximum cross-shore coverage. The continuous coverage of the entire coast as well as the regular frequency of the surveys make these data highly valuable for large-scale analysis and the establishment of geomorphological indicators to describe spatial variability of the inter-annual evolutions of the intertidal and supratidal beach systems along the coast. This contribution highlights the work carried out recently on the basis of LiDAR data for the implementation of semi-automatic methods to determine the coastline position as a synthetic indicator commonly used for beach evolution description. The advantages and limits related to automatic detection of coastline position will be developed. Other indicators of geomorphological evolution are studied at the scale of the sedimentary sub-cells of the Aquitanian sandy coast, in particular the differences in volumes between two years in the form of a sedimentary budget, the appearance of dune erosion scarps and, conversely, the formation of incipient foredunes, or the evolution of the dry beach width. These various indicators are related to the hydrodynamic variables and show the complexity of responses of the subaerial part of beach systems at regional scale.


Thomas Letan

Yann Régis-Gianas

Pierre Chifflier

Guillaume Hiet

Senter Sandman

Modular Verification of Programs with Effects and Effect Handlers in Coq

Keywords:

Modern computing systems have grown in complexity, and the attack surface has increased accordingly. Even though system components are generally carefully designed and even verified by different groups of people, the composition of these components is often regarded with less attention. This paves the way for "architectural attacks", a class of security vulnerabilities where the attacker is able to threaten the security of the system even if each of its components continues to act as expected. In this article, we introduce FreeSpec, a formalism built upon the key idea that components can be modelled as programs with algebraic effects to be realized by other components. FreeSpec allows for the modular modelling of a complex system, by defining idealized components connected together, and the modular verification of the properties of their composition. In addition, we have implemented a framework for the Coq proof assistant based on FreeSpec.

OS App

Introduction

A typical computing platform is made of dozens of hardware components, and some of them execute complex software stacks. In this context, building a secure computing system with respect to a given security policy remains challenging, because attackers will leverage any vulnerability they can find. Both local component flaws and components composition inconsistencies, that is, a mismatch between requirements assumed by some client components and the actual guarantees provided by others, can be used by attackers.

The latter scenario may lead to a situation where every component seems to be working as expected, but their composition creates an attack path. We name this class of security vulnerabilities "architectural attacks" [START_REF] Letan | SpecCert: Specifying and Verifying Hardware-based Security Enforcement[END_REF]. Over the past decade, many critical vulnerabilities affecting computing systems, in particular those relying on the x86 architecture, have raised awareness about the threat posed by architectural attacks. Figure 1 summarizes several significant attacks [START_REF] Wojtczuk | Attacking SMM Memory via Intel CPU Cache Poisoning[END_REF][START_REF] Duflot | Getting into the SMRAM: SMM Reloaded[END_REF][START_REF] Domas | The Memory Sinkhole[END_REF][START_REF] Kallenberg | Speed Racer: Exploiting an Intel Flash Protection Race Condition[END_REF][START_REF] Kovah | SENTER Sandman: Using Intel TXT to Attack Bioses[END_REF][START_REF] Stewin | Understanding DMA Malware[END_REF] inside an idealized view of an x86 computing platform. In all cases, the vulnerability was rooted in an inconsistency in the components' composition.

Fig. 1: Idealized x86 Computing Platform

The isolation of the System Management Mode (SMM) code by the hardware architecture is a good example to illustrate the threat posed by architectural attacks. The SMM is the most privileged execution mode of x86 CPU. Its purpose is to provide an "isolated processor environment that operates transparently to the operating system" [START_REF] Manual | Intel IA-64 Architecture Software Developer's Manual[END_REF] to execute so-called SMM code provided by the computer manufacturer. Since the SMM code is the most privileged software component executed by an x86 CPU, it is a desirable target for an attacker. The SMM code is stored in a dedicated memory region within the system memory, called the SMRAM; it is expected that only a CPU in SMM can access the SMRAM. In particular, the Memory Controller Hub (MCH) [START_REF]Intel: Intel 5100 Memory Controller Hub Chipset[END_REF] provides a security mechanism to that end. In 2009, Duflot et al. [START_REF] Duflot | Getting into the SMRAM: SMM Reloaded[END_REF] and Wojtczuk et al. [START_REF] Wojtczuk | Attacking SMM Memory via Intel CPU Cache Poisoning[END_REF] have independently shown that the cache could be used to circumvent this protection. The countermeasure required adding a new security mechanism to the CPU, meaning only computers produced after 2009 are protected against this particular vulnerability.

For many years, industrial manufacturers [START_REF] Reid | Who Guards the Guards? Formal Validation of the Arm v8-M Architecture Specification[END_REF][START_REF] Leslie-Hurd | Verifying Linearizability of Intel R Software Guard Extensions[END_REF] and researchers [START_REF] Chong | Report on the NSF Workshop on Formal Methods for Security[END_REF][START_REF] Choi | Kami: A Platform for High-Level Parametric Hardware Specification and Its Modular Verification[END_REF] have aimed to formally specify and verify hardware architectures. However, verifying properties of existing computing platforms poses significant challenges, because they tend to be both complex and under-specified; we are not aware of any model of an existing and broadly used computing system that is comprehensive in terms of its hardware and software components. Unfortunately, such a model is a prerequisite to verify a computing platform in terms of architectural attacks. The Coq proof assistant [START_REF]The Coq Proof Assistant[END_REF] has proven to be effective to model specific hardware components [START_REF] Braibant | Coquet: A Coq Library for Verifying Hardware[END_REF][START_REF] Morrisett | RockSalt: better, faster, stronger SFI for the x86[END_REF][START_REF] Choi | Kami: A Platform for High-Level Parametric Hardware Specification and Its Modular Verification[END_REF][START_REF] Jomaa | Formal Proof of Dynamic Memory Isolation Based on MMU[END_REF]. It provides a rich specification language, tools to write machine-checked proofs and a mechanism to derive executable programs to experimentally validate models. The scale of the task dictates several require-ments regarding the formalism to adopt in this particular case. It must allow for considering independently each component of our system, before composing them to conclude about the properties of the system as a whole.

This objective is reminiscent of the programming language problematic to model and verify large programs with side effects. Reasoning about side effects in purely functional languages such as Gallina, the Coq specification language, is difficult, firstly because they require somehow taking into account an outer stateful environment and secondly, because the composition of stateful computations is not well-handled by traditional (monadic) approaches. Algebraic effects and handlers [START_REF] Bauer | Programming with Algebraic Effects and Handlers[END_REF] are a generic approach overcoming this double challenge. They allow modelling large classes of effects (e.g., exception, state, non-determinism) and to compose effects within purely functional programs, while deferring the realizations of these effects to dedicated handlers.

In this paper, we aim to show how a variant of algebraic effects based on Free monads can be used to reason about large systems, by modelling their components as effect handlers. Our contribution is threefold:

-We propose an approach which leverages the key concepts of algebraic effects and handlers to model and to verify each component of a computing system independently, while providing the necessary abstractions to compose these components in order to verify the properties of the resulting system. -We have implemented FreeSpec5 , a framework for the Coq proof assistant to modularly verify programs with effects and effects handlers with our approach. -We have modelled and verified a simplified MCH with FreeSpec, in a first step towards illustrating how our formalism can be leveraged to tackle our initial objective, that is modelling and verifying computing platforms.

The rest of the paper proceeds as follows. We describe how we model components in terms of programs with effects and effect handlers (Section 2) and we introduce so-called abstract specifications to verify their respective properties (Section 3). We also discuss the current limitations of our approach in terms of components connection; FreeSpec works well with tree of components, when more complex connection patterns require more investigation. To illustrate our definitions, we use a running example in the form of the specification and verification of a simplified MCH. Then, we discuss how the different levels of composition of FreeSpec can be leveraged to scale the modelling and verification work for larger systems (Section 4). Finally, we detail how FreeSpec is in line with an ongoing effort to modularly verify both large systems and programs with effects (Section 5).

Modelling Programs with Effects

The first objective of FreeSpec is to incrementally model a complex system, one component at a time. To do so, we use the key concepts of algebraic effects and effect handlers, implemented with a variant of the Free monad called the Program monad as defined in the operational package of Haskell [START_REF] Apfelmus | The operational package[END_REF].

This section and the one afterwards proceed through a running example: a minimalist Memory Controller Hub (MCH) of the x86 hardware architecture. The MCH acts as a dispatcher for the CPU memory accesses; in our case, to the VGA controller or the DRAM controller. The MCH takes part in the isolation of the SMRAM, that is the special-purpose memory region inside the system memory which contains the SMM code. If correctly configured, the MCH will reroute any memory access which targets the SMRAM to the VGA controller, if this access is done by a CPU in another execution mode than SMM.

Interface of Effects

Within a computing system, interconnected components communicate through interfaces. A component which exhibits an interface receives computational requests from other components; it handles these requests by computing their results and sending the latter back to the client component. In FreeSpec, a computational request is modelled with an effect, that is a symbolic value which represents the request and its potential result.

Thereafter, we often define sets of values, and interfaces in particular, in terms of functions to construct these values. These functions are called "constructors" 6 , and they have mutually exclusive images, i.e. it is not possible to construct the same value with two different constructors. For I an interface, we denote by I| A ⊆ I the subset of effects whose results belong to a set A.

Example 1 (MCH Interfaces)

The VGA and the DRAM controllers exhibit a similar interface which allows reading and writing into a memory region. Their interfaces are denoted by I VGA and I DRAM respectively. Let Loc be the set of memory locations and Val the set of values stored inside the memory region. We use the value () to model effects without results (similarly to the void keyword in an imperative language). We define I DRAM (respectively I VGA ) with two constructors: The MCH interface is similar, but it distinguishes between privileged and unprivileged accesses. It also provides one effect to lock the SMRAM protection mechanism, i.e. it enables the SMRAM isolation until the next hardware reset. We define the set Priv { smm, unprivileged } to distinguish between privileged memory accesses made by a CPU in SMM and unprivileged accesses made the rest of the time. The MCH interface, denoted by I MCH , is defined with three constructors:

-Read DRAM : Loc → I DRAM | Val -Write DRAM : Loc → Val → I DRAM | {()} Then, I DRAM = I DRAM | {()} ∪ I DRAM | Val
-Read MCH : Loc → Priv → I MCH | Val -Write MCH : Loc → Val → Priv → I MCH | {()} -Lock : I MCH | {()}

Operational Semantics for Effects

An effect corresponds to a computational request made to an implementation of a given interface. For a given computational request, we define its operational semantics to compute its result. Ultimately, we will model a component as an operational semantics for all the effects of its interface. Since operational semantics are defined using a purely functional language, they always compute the same result for a given effect, which is inconsistent with the stateful aspect of hardware components. Thus, an operational semantics produces not only a result, but also a new operational semantics, which encapsulates the new state of the component.

Definition 1 (Operational Semantics). We write Σ I for the set of operational semantics for a given interface I, defined co-inductively as

Σ I { σ | σ : ∀A, I| A → A × Σ I }.
An operational semantics σ ∈ Σ I is a function which, given any effect of I, produces both a result which belongs to the expected set and a new operational semantics to use afterwards.

A component may use more than one interface. For instance, the MCH of our running example can access the system memory and the memory shared by the VGA controller. But an operational semantics is defined for only one interface. In FreeSpec, we solve this issue by composing interfaces together to create new ones.

Definition 2 (Interfaces Composition). Let I and J be two interfaces. ⊕ is the interface composition operator, defined with two constructors:

-InL : ∀A, I| A → (I ⊕ J )| A -InR : ∀A, J | A → (I ⊕ J )| A
The resulting interface I ⊕ J contains the effects of both I and J , wrapped into either InL or InR constructors, defined to preserve the effects results sets. Using ⊕, we can compose several interfaces together. We then need another composition operator, this time for operational semantics. We compose operational semantics together to construct a new operational semantics for the composed interface.

Definition 3 (Operational Semantics Composition). Let I and J be two interfaces, σ i ∈ Σ I and σ j ∈ Σ J be two operational semantics dedicated to these interfaces. In this article, we use the λ-calculus abstraction notation for functions. ⊗ is the composition operator for operational semantics, defined as

σ i ⊗ σ j λe. (x, σ i ⊗ σ j ) when e = InL(e i ) and σ i (e i ) = (x, σ i ) (x, σ i ⊗ σ j
) when e = InR(e j ) and σ j (e j ) = (x, σ j )

The definition of ⊗ has an important impact over what we can specify in FreeSpec. Handling an effect of I (respectively J ) does not interfere with σ j (respectively σ i ). As a consequence, we can only specify as-is trees of components, while graphs with, for instance, cycles or forward edges are still out of scope. This is the main limitation of FreeSpec, but its incidence is abated because computing platforms are often designed as a hierarchical succession of layers.

The Program Monad

Modelling programs with side effects in purely functional languages such as Gallina (the Coq specification language) or Haskell is usually achieved thanks to monads [START_REF] Hoareetal | Tackling the Awkward Squad: monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell[END_REF]. FreeSpec leverages a variant of the Free monad called the Program monad [START_REF] Apfelmus | The operational package[END_REF] to model programs with effects. Operational semantics play the role of operational [START_REF] Apfelmus | The operational package[END_REF] interpreters. We write P I (A) for the set of programs with effects which belongs to I, modelled thanks to the Program monad, and whose result belongs to a set A.

Definition 4 (Program Monad). P I (A) is defined with three constructors:

-Pure : A → P I (A) -Bind : ∀B, P I (B) → (B → P I (A)) → P I (A) -Request : I| A → P I (A)
These constructors allow for the construction of values which act similarly to abstract syntax trees to model programs with effects. On the one hand, Pure and Request are comparable to the leaves of a syntax tree and model atomic computations; Pure models local computations, whereas Request models deferring a computational request to a handler and waiting for its result. On the other hand, Bind (denoted by the infix operator > > = afterwards) models the control flow of a program with effects, like the abstract syntax tree nodes would. It defines how the result of one computation determines the following ones.

Example 3 (Copy) We define copy : Loc → Loc → P IDRAM ({()}) such that copy(l, l ) models a program with effects that returns no result, but copies the value v stored at the memory location l inside the memory location l .

copy(l, l ) Request(Read DRAM (l)) > > = λv.Request(Write DRAM (l , v))
Given l ∈ Loc and l ∈ Loc, copy(l, l ) symbolically models a program with effects. To assign an interpretation of this program, it must be completed with an operational semantics which realizes the interface I DRAM .

Definition 5 (Program With Effects Realization). Let I be an interface, σ ∈ Σ I an operational semantics for this interface and ρ ∈ P I (A) a program with effects which belong to this interface. σ[ρ] ∈ A × Σ I denotes the realization of this program by σ, defined as:

σ[ρ]    (x, σ) if ρ = Pure(x) σ(e) if ρ = Request(e) σ [f (y)] if ρ = q > > = f and (y, σ ) = σ[q] 2.

Components as Programs with Effects

With the interfaces, their operational semantics, the ⊕ and ⊗ operators to compose them and the Program monad to model programs with effects which belong to these interfaces, we now have all we need to model a given component which exposes an interface I and uses another interface J . We proceed with the following steps: modelling the component in terms of programs with effects, then deriving one operational semantics for I from these programs, assuming provided an operational semantics for J .

The behaviour of a component is often determined by a local, mutable state. When it computes the result of a computational request, not only a component may read its current state; but it can also modify it, for instance to handle the next computational request differently. This means we have to model the state of a component with a set S of symbolic state representations. We map the current state of the component and effects of I to a program with effects of J . These programs must compute the effect result and the new state of the component. Definition 6 (Component). Let I be the interface exhibited by a component and J the interface it uses. Let S be the set of its states. The component C, defined in terms of programs with effects of J , is of the form

∀A, I| A → S → P J (A × S)
Hence, C specifies how the component handles computational requests, both in terms of computation results and state changes.

Example 4 (Minimal MCH Model) Let C MCH be the MCH defined in terms of programs with effects of

I DRAM ⊕ I VGA , then C MCH is of the form ∀A, I MCH | A → S MCH → P IDRAM⊕IVGA (A × S MCH )
where S MCH {on, off} means the SMRAM protection is either activated (on) or deactivated (off).

One the one hand, the Lock effect will activate the isolation mechanism of the MCH, setting its state to on. On the other hand, the effects constructed with Read MCH and Write MCH will use the current state of the MCH, the privileged parameter of the effect and the memory location to lookup to determine if it uses the DRAM or the VGA controller. By default, it fetches the memory of the DRAM controller, except if the isolation mechanism is activated, the access is unprivileged and the targeted memory location belongs to the SMRAM. In such a case, it reroutes access to the VGA controller.

A component C defined in terms of programs with effects cannot be used as-is to compute the result of a given effect. To do that, we need to derive an operational semantics for I from C. Definition 7 (Deriving Operational Semantics). Let C be a component which exhibits an interface I, uses an interface J and whose states belong to S. Let s ∈ S be the current state of the component and σ j ∈ Σ J be an operational semantics for J . We can derive an operational semantics for I, denoted by C, s, σ j , defined as C, s, σ j λi.(x, C, s , σ j ) where ((x, s ),

σ j ) = σ j [C(i, s)]
The resulting operational semantics models a system made of interconnected components, and can then be used to derive another component model into an operational semantics which models a larger system. For instance, we can proceed with the following steps to comprehensively model our running example: (i) defining the operational semantics for the DRAM and VGA controllers; (ii) using these operational semantics to derive an operational semantics from C MCH . The resulting operational semantics can take part in the derivation of a cache defined in terms of programs with effects of I MCH , to model a larger part of the system pictured in the Figure 1.

Modular Verification of Programs with Effects

The first objective of FreeSpec is to provide the required tools to model each component of a system independently, and to compose these components to model the whole system. Its second objective is to verify that the composition of several components satisfies a set of properties. To achieve that, we introduce the so-called abstract specifications, which allows for specifying, for each interface, expected properties for the effect results, independently of any underlying handler. Abstract specifications can be used to emphasize the responsibility of each component of a system regarding the enforcement of a given security policy. Verifying a component is done against abstract specifications of the interfaces it directly uses, even if it relies on a security property enforced by a deeper component in the components graph. In this case, we have to verify that every single component which separate them preserve this property. This procedure can help to prevent or uncover architectural attacks.

In this section, we proceed with our running example by verifying that the MCH correctly isolates the SMRAM. In order to do that, we define an abstract specification which states that privileged reads targeting the SMRAM returns the value which has previously been stored by a privileged write. It models the SMRAM isolation: unprivileged writes cannot tamper with the content of the SMRAM, as read by a privileged CPU.

Definition

In FreeSpec, an abstract specification dedicated to an interface I is twofold. It defines a precondition over the effects that a caller must satisfy; and, in return, it specifies a postcondition over the effects results that an operational semantics must enforce. Since both the precondition and the postcondition may vary in time, we parameterize an abstraction specification with an abstract state and a step function to update this state after each effect realization. Definition 8 (Abstract Specification). We write A for an abstract specification dedicated to an interface I, defined as a tuple Ω, step, pre, post where -Ω is a set of abstract states step : ∀A, I| A → A → Ω → Ω is a transition function for the abstract state.

pre ⊆ I × Ω is the precondition over effects, such that (e, ω) ∈ pre if and only if the effect e satisfies the precondition parameterized with the abstract state ω (denoted by pre(e, ω)). post ⊆ A (I| A × A × Ω) is the postcondition over effects results, such that (e, x, ω) ∈ post if and only if the results x computed for the effects e satisfies the postcondition parameterized with the abstract state ω (denoted by post(e, x, ω)).

By defining an abstract specification of an interface I, it becomes possible to abstract away the effect handler, i.e. the underlying component. As a consequence, reasoning about a program with effects can be achieved without the need to look at the effect handlers. An abstract specification is dedicated to one verification problem (in our context, one security property), and it is possible to define as many abstraction specifications as required.

We write run step : ∀A, Σ I → P I (A) → Ω → (A × Σ I × Ω) for the function which, in addition to realize a program with effects, updates an abstract state after each effect. Using run step , we can determine both the precondition over effects and the postcondition over effects results while an operational semantics realizes a program with effects.

Example 5 (MCH Abstract Specification) Let A MCH be the abstract specification such that A MCH = Ω MCH , step MCH , pre MCH , post MCH . A MCH models the following property: "privileged reads targeting the SMRAM return the value which has been previously stored by a privileged write":

-Let Smram ⊆ Loc be the set of memory locations which belong to the SMRAM.

We define Ω MCH Smram → Val , such that ω ∈ Ω MCH models a view of the SMRAM as exposed by the MCH for privileged reads.

-We define step MCH which updates the view of the MCH (modelled as a function) after each privileged write access targeting any SMRAM location l, that is

step MCH (e, x, ω)    λl . (if l = l then v else ω(l )) if e = Write MCH (l, v, smm) and l ∈ Smram ω otherwise
-There is no precondition to the use of the MCH effects, so

∀e ∈ I, ∀ω ∈ Ω MCH , pre MCH (e, ω)
-The postcondition enforces that the result x of a privileged read targeting the SMRAM (Read(l, smm)) has to match the value stored in A MCH abstract state, i.e. the expected content for this memory location ω(l).

post MCH (e, x, ω) ∀l ∈ Loc, e = Read MCH (l, smm) ∧ l ∈ Smram ⇒ x = ω(l)

Compliance and Correctness

The verification of a component C, which exhibits I and uses J , consists in proving we can derive an operational semantics σ i for I from an operational semantics σ j for J . This semantics σ i enforces the postcondition of an abstract specification A I dedicated to I (compliance). As C is defined in terms of programs with effects of J , the latter needs to make a legitimate usage of J with respect to an abstract specification A J dedicated to J (correctness). First, σ i complies with A I if, (1) given any effect which satisfies A I precondition, σ i produces a result which satisfies its postcondition, and if (2) the new operational semantics σ i also complies with A I . The precondition and the postcondition are parameterized by an abstract state, so is the compliance property. Secondly, programs with effects of C make a legitimate usage of an operational semantics σ j ∈ Σ J which complies with A J if they only use effects which satisfy A J precondition. As for the compliance property, correctness is parameterized with an abstract state.

Definition 10 (Program With Effects Correctness).

Let A be an abstract specification for an interface I, defined as Ω, step, pre, post , ω ∈ Ω, and ρ ∈ P I (A), then ρ is correct with respect to A in accordance with ω (denoted by

A[ω] | = ρ), iff. A[ω] | = ρ            True if ρ = Pure(x) pre(e, ω) if ρ = Request(e) ∀σ ∈ Σ I such that σ |= A[ω], A[ω] | = q ∧ A[ω ] | = f (x) if ρ = q > > = f where (x, _, ω ) = run step J (σ, q, ω)
Every local computation (Pure) is correct with respect to A in accordance with ω. A computation which uses an effect e ∈ I (Request) is correct with respect to A in accordance with ω if and only if e satisfies the precondition of A for the abstract state ω. Finally, the chaining of two programs with effects (Bind) is correct with A in accordance with ω if the first program is correct with A in accordance with ω, and the second program is correct in accordance with the abstract state reached after the realization of the first program.

Properties, inferred from an abstract specification, of a correct program with effects only hold if it is realized by a compliant operational semantics. Besides, we prove that correct programs preserve operational semantics compliance.

Theorem 1 (Compliance Preservation). Let A be an abstract specification dedicated to an interface I. σ a compliant operational semantics for I produces a compliant operational semantics σ if it realizes a correct program ρ, that is

σ |= A[ω] ∧ A[ω] | = ρ ⇒ σ |= A[ω ] where run step (σ, ρ, ω) = (x, σ , ω )
As for interfaces (with ⊕) and operational semantics (with ⊗), we have also defined an abstract specification composition operator . We do not detail its definition in this article, but it has the significant property of allowing for reasoning about the composition of interfaces and composition of operational semantics.

Theorem 2 (Congruent Composition). Let I (respectively J ) be an interface. Let A I (respectively A J ) be an abstract specification and σ i ∈ Σ I (respectively σ j ∈ Σ J ) be an operational semantics for this interface.

σ i |= A I [ω i ] ∧ σ j |= A J [ω j ] ⇒ σ i ⊗ σ j |= (A I A J )[ω i , ω j ]
With the Compliance Preservation, we know that as long as we follow the abstract specification precondition related to the effects we use, compliant operational semantics keep enforcing the postcondition. With the Compliance Preservation and Congruent Composition, we know we can reason locally, that is component by component.

Proofs Techniques to Show Compliance For Components

We have dived into the mechanisms which allow for composing together compliant operational semantics, but little has been said about how to prove the compliance property to begin with. In a typical FreeSpec use case, operational semantics are not built as-is, but rather derived from a component model (Definition 7). How to prove the resulting operational semantics complies with an abstract specification depends on how the component is connected to the rest of the system. We have already discussed the consequences of the operational semantics composition operator ⊗ (Definition 3). Notably, a graph of components which connects two nodes with more than one path cannot be easily modelled and verified in FreeSpec. In its current state, FreeSpec provides some theorems to verify the properties of a component model in terms of an abstract specification, depending on the composition pattern.

The most composition connection pattern consists of one component which uses many components, and is only used by one other component. Let I and J be two interfaces and let C, a component with a set of possible states S, which exhibits I and uses J . Let A I be an abstract specification dedicated to I. Deriving an operational semantics from C which complies with A I in accordance with ω i ∈ Ω I requires to show the existence of s ∈ S and σ j ∈ Σ J such that

C, s, σ j |= A I [ω i ].
However, proving this statement would not be very satisfying, as it ties our verification results to one specific operational semantics σ j , and by extension one specific component. As a consequence, we define an abstract specification A J to generalize our statement and abstracting away σ j . We now need to prove it exists ω j ∈ Ω J such that given an operational semantics σ j which complies with A J in accordance with ω j , the operational semantics derived from C, s and σ j complies with A I in accordance with ω i , that is

∀σ j ∈ Σ J , σ j |= A J [ω j ] ⇒ C, s, σ j |= A I [ω i ]
The combinatorial explosion of cases introduced by ω i , s and ω j , modified as the component handles effects, makes inductive reasoning challenging. The FreeSpec framework provides a useful theorem to address these challenges, which leverages a so-called predicate of synchronization. The latter is defined by the user on a case-by-case basis, to act as an invariant for the induction, and a sufficient condition to enforce compliance.

Theorem 3 (Derivation Compliance). Let sync, a relation between abstract states of Ω I and Ω J , states of S, be a predicate of synchronization. Then, it is expected that, ∀ω i ∈ Ω I , s ∈ S and ω j ∈ Ω J such that sync(ω i , s, ω j ) holds, then ∀σ j ∈ Σ J such that σ j |= A J [ω j ] and ∀e ∈ I such that pre I (e, ω i ), 1. C preserves the synchronization of states, that is sync(ω i , s , ω j ) 2. C is defined in terms of programs with effects which are correct with respect to A J in accordance with ω j , that is A J [ω j ] | = C(e, s) 3. C computes a result for e which satisfies A I postcondition, that is post I (e, x, ω i ) where ((x, s ), σ j , ω j ) = run step J (σ j , C(e, s), ω j ) and ω i = step I (e, x, ω i ). Should these three properties be verified, then we show that

sync(ω i , s, ω j ) ∧ σ j |= A J [ω j ] ⇒ C, s, σ j |= A I [ω i ].
Example 6 (MCH Compliance) We want to prove we can derive an operational semantics from C MCH (Example 4) which complies with A MCH (Example 5).

We define A DRAM Ω DRAM , step DRAM , pre DRAM , post DRAM an abstract specification dedicated to I DRAM to express the following property: "a read access to a memory location which belongs to the SMRAM return the value which have been previously written at this memory location." In particular, Ω DRAM = Ω MCH , i.e. they are two views of the SMRAM, as exposed by the DRAM controller or by the MCH. In this context, the behaviour of VGA is not relevant. Let be the abstract specification which has no state and such that its precondition and postcondition are always satisfied (meaning every operational semantics always complies with it). Therefore, the abstract specifications dedicated to the interface used by C MCH , that is I DRAM ⊕I VGA , is A DRAM whose abstract state is Ω DRAM .

We define the predicate of synchronization sync MCH such that

sync MCH (ω i , s, ω j ) s = on ∧ ∀l ∈ Smram, ω i (l) = ω j (l)
Hence, we start our reasoning from a situation where the SMRAM isolation is already activated and the states of the two abstract specifications are the same, meaning the two views of the SMRAM (as stored in the DRAM, and as exposed by the MCH) coincide. We prove sync MCH satisfies the three premises of the Theorem 3. We conclude we can derive an operational semantics from C MCH which complies with A MCH .

Another common composition pattern consists of a component which is used by more than one other component. FreeSpec provides a theorem which allows for extending the result obtained with the Theorem 3, in the specific case where concurrent accesses do not lead to any change of the abstract state.

Discussion

For two sections, we have introduced the FreeSpec key definitions and theorems so that we could model a minimal MCH component and verify its properties in the presence of a well-behaving DRAM controller. This example has been driven by a real mechanism commonly found inside x86-based computing platforms. We now discuss how FreeSpec can be leveraged to model and verify larger systems.

FreeSpec as a Methodology

The typical workflow of FreeSpec can be summarized as follows: specifying the interfaces of a system; modelling the components of the system in terms of programs with effects of these interfaces; identifying the abstract specifications which express the requirements over each interface; verifying each component in terms of compliance with these abstract specifications.

Independent groups of people can use FreeSpec to modularly model and verify a system, as long as they agree on the interfaces and abstract specifications. If, during the verification process, one group finds out a given interface or abstract specification needs to be updated, the required modifications may impact its neighbours. For instance, modelling a x86-based computing system, as pictured in Figure 1, using FreeSpec requires to take into account the CPU cache, and to verify it complies with an abstract specification similar to the one defined in Example 5. Thus, FreeSpec could have helped uncover the attack mentioned in Section 1 [START_REF] Wojtczuk | Attacking SMM Memory via Intel CPU Cache Poisoning[END_REF][START_REF] Duflot | Getting into the SMRAM: SMM Reloaded[END_REF], and other similar architectural attacks.

The abstract specifications are defined in terms of interfaces, i.e. independently from components. It has two advantages. First, for a given verification problem modelled with a set of abstract specifications, two components which exhibit the same interface can be proven to comply with the same abstract specification. In such a case, we can freely interchange these components, and the verification results remain true. This is useful to consider the challenge posed by components versioning, i.e. a new version of a component brings new features which could be leveraged by an attacker. Then, it is possible to verify a given component in terms of several abstract specifications. This means we can independently conduct several verification works against the same component.

FreeSpec as a Framework

FreeSpec includes about 8,000 lines of code: 6,000 for its core, 2,000 for the experiments. It has been built upon three objectives: readability of models, automation of proofs, opportunity to extract these models for experimental validation.

To achieve readability, FreeSpec borrows several popular concepts to modern functional programming language, such as Haskell. We have used the Notation feature of Coq to add the do-notation of Haskell to Gallina. This allows for writing monadic functions that can be read as if it were pseudo-code. The readers familiar with the monad transformers mechanism [START_REF] Liang | Monad transformers and modular interpreters[END_REF] may also have recognized the definition of the transformer variant of the State monad in the Definition 6. FreeSpec takes advantage of the State monad mechanism to seamlessly handle the local state of the component.

To achieve automation of proofs, we have developed specific Coq tactics. Some definitions of FreeSpec can be pretty verbose, and the proofs quickly become difficult to manage as the program grows in complexity. FreeSpec provides two tactics to explore the control flow of programs with effects.

Finally, to achieve model extraction, we have defined the key concepts of FreeSpec so that they remain compatible with the extraction mechanism of Coq. As a consequence, component models can be derived into executable programs. For a hardware component, it means we could, for instance, compare its behaviour with its concrete counterpart. For a software component, it means we can fill the gap between the model and the implementation.

Related Work

FreeSpec falls within two domains of research: the verification of large systems made of components, and the modular verification of programs with effects.

FreeSpec follows our previous work named SpecCert [START_REF] Letan | SpecCert: Specifying and Verifying Hardware-based Security Enforcement[END_REF], whose lack of modularity complexified scalability. Kami [START_REF] Choi | Kami: A Platform for High-Level Parametric Hardware Specification and Its Modular Verification[END_REF] shares many concepts with FreeSpec, but implements them in a totally different manner: components are defined as labelled transition systems and can be extracted into FPGA bitstreams. Kami is hardware-specific, thus is not suitable to reason about systems which also include software components. However, it allows for expressing more composition pattern than FreeSpec (e.g. components cycle). Thomas Heyman et al. [START_REF] Heyman | Reusable Formal Models for Secure Software Architectures[END_REF] have proposed a component-based modelling technique for Alloy [START_REF] Jackson | Software Abstractions: Logic, Language and Analysis[END_REF], where components are primarily defined as semantics for a set of operations; a component is connected to another when it leverages its operations. Alloy leverages a model finder to verify a composition of these components against known security patterns, and to assume or verify facts about operations semantics; however, it lacks an extraction mechanism, which makes it harder to validate the model.

Algebraic effects and effect handlers led to a lot of research about verification of programs with side effects [START_REF] Bauer | Programming with Algebraic Effects and Handlers[END_REF][START_REF] Brady | Resource-dependent algebraic effects[END_REF], but to our surprise, we did not find any approach to write and verify programs with effects and effect handlers written for Gallina. However, other approaches exist. Ynot [START_REF] Nanevski | Ynot: Dependent Types for Imperative Programs[END_REF] is a framework for the Coq proof assistant to write, reason with and extract Gallina programs with side effects. Ynot side effects are specified in terms of Hoare preconditions and postconditions parameterized by the program heap, and does not dissociate the definition of an effect and properties over its realization. To that extent, FreeSpec abstract specification is more expressive (thanks to the abstract state) and flexible (we can define more than one abstract specification for a given interface). Claret et al. have proposed Coq.io, a framework to specify and verify interactive programs in terms of use cases [START_REF] Claret | Mechanical Verification of Interactive Programs Specified by Use Cases[END_REF]. The proofs rely on scenarios which determine how an environment would react to the program requests. These scenarios are less generic and expressive than FreeSpec abstract specifications, but they are declarative and match a widely adopted software development process. As a consequence, they may be easier to read and understand for software developers.

Previous approaches from the Haskell community to model programs with effects using Free monads [START_REF] Apfelmus | The operational package[END_REF][START_REF] Kiselyov | Freer Monads, More Extensible Effects[END_REF] are the main source of inspiration for FreeSpec. In comparison, we provide a novel method to verify these programs, inspired by the interface refinement of the B-method [START_REF] Abrial | The B-Book: Assigning Programs to Meanings[END_REF]. It also had some similiraties with FoCaLiZe [START_REF] Pessaux | FoCaLiZe: inside an F-IDE[END_REF], a proof environment where proofs are attached to components.

Conclusion & Future Work

We have proposed an approach to model and verify each component of a computing system independently, while providing the necessary abstractions to compose these components together in order to verify the properties of the resulting system. We have implemented FreeSpec, an open-source framework for the Coq proof assistant which implements our approach. Finally, we applied our approach to a simplified x86-based computing platform in terms of programs.

We would like to consider more composition patterns. We also anticipate abstract specifications may become harder to understand as their complexity grows. We want to make them more declarative, so they could be more easily understood by software developers who are less familiar with functional programming and formal verification.

  , and Read DRAM (l) ∈ I DRAM | Val is an effect that describes a memory access to read the value v ∈ Val stored at the location l ∈ Loc.

Example 2 (

 2 VGA and DRAM Composition) We consider I DRAM ⊕I VGA . Then, InL(Read DRAM (l)) ∈ (I DRAM ⊕ I VGA )| Val is an effect that describes a read access targeting the DRAM controller, whereas InR(Write VGA (l, c)) ∈ (I DRAM ⊕ I VGA )| {()} is an effect that describes a write access targeting the VGA controller.

Definition 9 (

 9 Operational Semantics Compliance). Let A be an abstract specification for an interface I, defined as Ω, step, pre, post , ω ∈ Ω, then σ ∈ Σ I complies with A in accordance with ω (denoted by σ |= A[ω]) iff. ∀e ∈ I, pre(e, ω) ⇒ post(e, x, ω) ∧ σ |= A[step(e, x, ω)] where (x, σ ) = σ(e)

FreeSpec has been released as a free software, under the terms of the GPLv3. https: //github.com/ANSSI-FR/FreeSpec

In this article, functions are written in bold. In addition, constructors begin with a capital letter.