Publications
Cross-language attacks
April 22, 2022
Conference Paper
Published in:
Network and Distributed System Security (NDSS) Symposium 2022.
Topic:
R&D area:
R&D group:
Summary
Memory corruption attacks against unsafe programming languages like C/C++ have been a major threat to computer systems for multiple decades. Various sanitizers and runtime exploit mitigation techniques have been shown to only provide partial protection at best. Recently developed ‘safe’ programming languages such as Rust and Go hold the promise to change this paradigm by preventing memory corruption bugs using a strong type system and proper compile-time and runtime checks. Gradual deployment of these languages has been touted as a way of improving the security of existing applications before entire applications can be developed in safe languages. This is notable in popular applications such as Firefox and Tor. In this paper, we systematically analyze the security of multi-language applications. We show that because language safety checks in safe languages and exploit mitigation techniques applied to unsafe languages (e.g., Control-Flow Integrity) break different stages of an exploit to prevent control hijacking attacks, an attacker can carefully maneuver between the languages to mount a successful attack. In essence, we illustrate that the incompatible set of assumptions made in various languages enables attacks that are not possible in each language alone. We study different variants of these attacks and analyze Firefox to illustrate the feasibility and extent of this problem. Our findings show that gradual deployment of safe programming languages, if not done with extreme care, can indeed be detrimental to security.
Summary
Memory corruption attacks against unsafe programming languages like C/C++ have been a major threat to computer systems for multiple decades. Various sanitizers and runtime exploit mitigation techniques have been shown to only provide partial protection at best. Recently developed ‘safe’ programming languages such as Rust and Go hold the promise...
READ MORE
Preventing Kernel Hacks with HAKCs
April 22, 2022
Conference Paper
Published in:
Network and Distributed System Security (NDSS) Symposium 2022.
Topic:
R&D area:
R&D group:
Summary
Commodity operating system kernels remain monolithic for practical and historical reasons. All kernel code shares a single address space, executes with elevated processor privileges, and has largely unhindered access to all data, including data irrelevant to the completion of a specific task. Applying the principle of least privilege, which limits available resources only to those needed to perform a particular task, to compartmentalize the kernel would realize major security gains, similar to microkernels yet without the major redesign effort. Here, we introduce a compartmentalization design, called a Hardware-Assisted Kernel Compartmentalization (HAKC), that approximates least privilege separation, while minimizing both developer effort and performance overhead. HAKC divides code and data into separate partitions, and specifies an access policy for each partition. Data is owned by a single partition, and a partition’s access-control policy is enforced at runtime, preventing unauthorized data access. When a partition needs to transfer control flow to outside itself, data ownership is transferred to the target, and transferred back upon return. The HAKC design allows for isolating code and data from the rest of the kernel, without utilizing any additional Trusted Computing Base while compartmentalized code is executing. Instead, HAKC relies on hardware for enforcement. Loadable kernel modules (LKMs), which dynamically load kernel code and data providing specialized functionality, are the single largest part of the Linux source base. Unfortunately, their collective size and complexity makes LKMs the cause of the majority of CVEs issued for the Linux kernel. The combination of a large attack surface in kernel modules, and the monolithic design of the Linux kernel, make LKMs ideal candidates for compartmentalization. To demonstrate the effectiveness of our approach, we implement HAKC in Linux v5.10 using extensions to the Arm v8.5-A ISA, and compartmentalize the ipv6.ko LKM, which consists of over 55k LOC. The average overhead measured in Apachebench tests was just 1.6%–24%. Additionally, we compartmentalize the nf_tables.ko packet filtering LKM, and measure the combined impact of using both LKMs. We find a reasonable linear growth in overhead when both compartmentalized LKMs are used. Finally, we measure no significant difference in performance when using the compartmentalized ipv6.ko LKM over the unmodified LKM during real-world web browsing experiments on the Alexa Top 50 websites.
Summary
Commodity operating system kernels remain monolithic for practical and historical reasons. All kernel code shares a single address space, executes with elevated processor privileges, and has largely unhindered access to all data, including data irrelevant to the completion of a specific task. Applying the principle of least privilege, which limits...
READ MORE
System analysis for responsible design of modern AI/ML systems
April 19, 2022
Journal Article
Published in:
arXiv, April 19, 2022.
Summary
The irresponsible use of ML algorithms in practical settings has received a lot of deserved attention in the recent years. We posit that the traditional system analysis perspective is needed when designing and implementing ML algorithms and systems. Such perspective can provide a formal way for evaluating and enabling responsible ML practices. In this paper, we review components of the System Analysis methodology and highlight how they connect and enable responsible practices of ML design.
Summary
The irresponsible use of ML algorithms in practical settings has received a lot of deserved attention in the recent years. We posit that the traditional system analysis perspective is needed when designing and implementing ML algorithms and systems. Such perspective can provide a formal way for evaluating and enabling responsible...
READ MORE
COVID-19 exposure notification in simulated real-world environments
April 15, 2022
Project Report
Published in:
MIT Lincoln Laboratory Report ACTA-3
Summary
Privacy-preserving contact tracing mobile applications, such as those that use the Google-Apple Exposure Notification (GAEN) service, have the potential to limit the spread of COVID-19 in communities, but the privacy-preserving aspects of the protocol make it difficult to assess the performance of the apps in real-world populations. To address this gap, we exercised the CovidWatch app on both Android and iOS phones in a variety of scripted realworld scenarios, relevant to the lives of university students and employees. We collected exposure data from the app and from the lower-level Android service, and compared it to the phones' actual distances and durations of exposure, to assess the sensitivity and specificity of the GAEN service configuration as of February 2021. Based on the app's reported ExposureWindows and alerting thresholds for Low and High alerts, our assessment is that the chosen configuration is highly sensitive under a range of realistic scenarios and conditions. With this configuration, the app is likely to capture many long-duration encounters, even at distances greater than six feet, which may be desirable under conditions with increased risk of airborne transmission.
Summary
Privacy-preserving contact tracing mobile applications, such as those that use the Google-Apple Exposure Notification (GAEN) service, have the potential to limit the spread of COVID-19 in communities, but the privacy-preserving aspects of the protocol make it difficult to assess the performance of the apps in real-world populations. To address this...
READ MORE
The Simulation of Automated Exposure Notification (SimAEN) Model
April 15, 2022
Project Report
Published in:
MIT Lincoln Laboratory Report ACTA-5
Topic:
Summary
Automated Exposure Notication (AEN) was implemented in 2020 to supplement traditional contact tracing for COVID-19 by estimating "too close for too long" proximities of people using the service. AEN uses Bluetooth messages to privately label and recall proximity events, so that persons who were likely exposed to SARS-CoV-2 can take the appropriate steps recommended by their health care authority. This paper describes an agent-based model that estimates the effects of AEN deployment on COVID-19 caseloads and public health workloads in the context of other critical public health measures available during the COVID-19 pandemic. We selected simulation variables pertinent to AEN deployment options, varied them in accord with the system dynamics available in 2020-2021, and calculated the outcomes of key metrics across repeated runs of the stochastic multi-week simulation. SimAEN's parameters were set to ranges of observed values in consultation with public health professionals and the rapidly accumulating literature on COVID-19 transmission; the model was validated against available population-level disease metrics. Estimates from SimAEN can help public health officials determine what AEN deployment decisions (e.g., configuration, workflow integration, and targeted adoption levels) can be most effective in their jurisdiction, in combination with other COVID-19 interventions (e.g., mask use, vaccination, quarantine and isolation periods).
Summary
Automated Exposure Notication (AEN) was implemented in 2020 to supplement traditional contact tracing for COVID-19 by estimating "too close for too long" proximities of people using the service. AEN uses Bluetooth messages to privately label and recall proximity events, so that persons who were likely exposed to SARS-CoV-2 can take...
READ MORE
Bluetooth Low Energy (BLE) Data Collection for COVID-19 Exposure Notification
April 13, 2022
Project Report
Published in:
MIT Lincoln Laboratory Report ACTA-2
Summary
Privacy-preserving contact tracing mobile applications, such as those that use the Google-Apple Exposure Notification (GAEN) service, have the potential to limit the spread of COVID-19 in communities; however, the privacy-preserving aspects of the protocol make it difficult to assess the performance of the Bluetooth proximity detector in real-world populations. The GAEN service configuration of weights and thresholds enables hundreds of thousands of potential configurations, and it is not well known how the detector performance of candidate GAEN configurations maps to the actual "too close for too long" standard used by public health contact tracing staff. To address this gap, we exercised a GAEN app on Android phones at a range of distances, orientations, and placement configurations (e.g., shirt pocket, bag, in hand), using RF-analogous robotic substitutes for human participants. We recorded exposure data from the app and from the lower-level Android service, along with the phones' actual distances and durations of exposure.
Summary
Privacy-preserving contact tracing mobile applications, such as those that use the Google-Apple Exposure Notification (GAEN) service, have the potential to limit the spread of COVID-19 in communities; however, the privacy-preserving aspects of the protocol make it difficult to assess the performance of the Bluetooth proximity detector in real-world populations. The...
READ MORE
Fast decomposition of temporal logic specifications for heterogeneous teams
April 1, 2022
Journal Article
Published in:
IEEE Robot. Autom. Lett., Vol. 7, No. 2, April 2022, pp. 2297-2304.
Topic:
R&D group:
Summary
We focus on decomposing large multi-agent path planning problems with global temporal logic goals (common to all agents) into smaller sub-problems that can be solved and executed independently. Crucially, the sub-problems' solutions must jointly satisfy the common global mission specification. The agents' missions are given as Capability Temporal Logic (CaTL) formulas, a fragment of Signal Temporal Logic (STL) that can express properties over tasks involving multiple agent capabilities (i.e., different combinations of sensors, effectors, and dynamics) under strict timing constraints. We jointly decompose both the temporal logic specification and the team of agents, using a satisfiability modulo theories (SMT) approach and heuristics for handling temporal operators. The output of the SMT is then distributed to subteams and leads to a significant speed up in planning time compared to planning for the entire team and specification. We include computational results to evaluate the efficiency of our solution, as well as the trade-offs introduced by the conservative nature of the SMT encoding and heuristics.
Summary
We focus on decomposing large multi-agent path planning problems with global temporal logic goals (common to all agents) into smaller sub-problems that can be solved and executed independently. Crucially, the sub-problems' solutions must jointly satisfy the common global mission specification. The agents' missions are given as Capability Temporal Logic (CaTL)...
READ MORE
Quantifying bias in face verification system
April 1, 2022
Journal Article
Published in:
Comput. Sci. Math. Forum 2022, 3(1), 6
Topic:
R&D area:
Summary
Machine learning models perform face verification (FV) for a variety of highly consequential applications, such as biometric authentication, face identification, and surveillance. Many state-of-the-art FV systems suffer from unequal performance across demographic groups, which is commonly overlooked by evaluation measures that do not assess population-specific performance. Deployed systems with bias may result in serious harm against individuals or groups who experience underperformance. We explore several fairness definitions and metrics, attempting to quantify bias in Google’s FaceNet model. In addition to statistical fairness metrics, we analyze clustered face embeddings produced by the FV model. We link well-clustered embeddings (well-defined, dense clusters) for a demographic group to biased model performance against that group. We present the intuition that FV systems underperform on protected demographic groups because they are less sensitive to differences between features within those groups, as evidenced by clustered embeddings. We show how this performance discrepancy results from a combination of representation and aggregation bias.
Summary
Machine learning models perform face verification (FV) for a variety of highly consequential applications, such as biometric authentication, face identification, and surveillance. Many state-of-the-art FV systems suffer from unequal performance across demographic groups, which is commonly overlooked by evaluation measures that do not assess population-specific performance. Deployed systems with bias...
READ MORE
Probabilistic coordination of heterogeneous teams from capability temporal logic specifications
April 1, 2022
Journal Article
Published in:
IEEE Robot. Autom. Lett., Vol. 7, No. 2, April 2022, pp. 1190-7.
Topic:
R&D group:
Summary
This letter explores coordination of heterogeneous teams of agents from high-level specifications. We employ Capability Temporal Logic (CaTL) to express rich, temporal-spatial tasks that require cooperation between many agents with unique capabilities. CaTL specifies combinations of tasks, each with desired locations, duration, and set of capabilities, freeing the user from considering specific agent trajectories and their impact on multi-agent cooperation. CaTL also provides a quantitative robustness metric of satisfaction based on availability of required capabilities for each task. The novelty of this letter focuses on satisfaction of CaTL formulas under probabilistic conditions. Specifically, we consider uncertainties in robot motion (e.g., agents may fail to transition between regions with some probability) and local probabilistic workspace properties (e.g., if there are not enough agents of a required capability to complete a collaborative task). The proposed approach automatically formulates amixed-integer linear program given agents, their dynamics and capabilities, an abstraction of the workspace, and a CaTL formula. In addition to satisfying the given CaTL formula, the optimization considers the following secondary goals (in decreasing order of priority): 1) minimize the risk of transition failure due to uncertainties; 2) maximize probabilities of regional collaborative satisfaction (if there is an excess of agents); 3) maximize the availability robustness of CaTL for potential agent attrition; 4) minimize the total agent travel time. We evaluate the performance of the proposed framework and demonstrate its scalability via numerical simulations.
Summary
This letter explores coordination of heterogeneous teams of agents from high-level specifications. We employ Capability Temporal Logic (CaTL) to express rich, temporal-spatial tasks that require cooperation between many agents with unique capabilities. CaTL specifies combinations of tasks, each with desired locations, duration, and set of capabilities, freeing the user from...
READ MORE
Wearable technology in extreme environments
March 14, 2022
Book Chapter
Published in:
Chapter 2 in: Cibis, T., McGregor AM, C. (eds) Engineering and Medicine in Extreme Environments. Springer, Cham. https://doi.org/10.1007/978-3-030-96921-9_2
Topic:
R&D area:
R&D group:
Summary
Humans need to work in many types of extreme environments where there is a need to stay safe and even to improve performance. Examples include: medical providers treating infectious disease, people responding to other biological or chemical hazards, firefighters, astronauts, pilots, divers, and people working outdoors in extreme hot or cold temperatures. Wearable technology is ubiquitous in the consumer market but is still needed for extreme environments. For these applications, it is particularly challenging to meet requirements to be actionable, accurate, acceptable, integratable, and affordable. To provide insight into these needs and possible solutions and the technology trade-offs involved, several examples are provided. A physiological monitoring example is described for predicting and avoiding heat injury. A cognitive monitoring example is described for estimating cognitive workload, with broader applicability to a variety of conditions, such as cognitive fatigue and depression. Finally, eye tracking is considered as a promising wearable sensing modality with applications for both physiological and cognitive monitoring. Concluding thoughts are offered on the compelling need for wearable technology in the face of pandemics, wildfires, and climate change, but also for global projects that can uplift mankind, such as long-duration spaceflight and missions to Mars.
Summary
Humans need to work in many types of extreme environments where there is a need to stay safe and even to improve performance. Examples include: medical providers treating infectious disease, people responding to other biological or chemical hazards, firefighters, astronauts, pilots, divers, and people working outdoors in extreme hot or...
READ MORE