Search for: All records

Transnational municipal networks (TMNs) have been heralded as actors that can avert a climate catastrophe by filling the “emission gaps” left by national climate policies. But can these networks reduce the carbon pollution of power plants, the world’s largest sites of climate-disrupting emissions? Using an international data source on individual power plants, we empirically analyze this issue. Findings reveal that after accounting for their structural properties and the national policies to which they are subject, power plants emit less CO₂when nested in cities that are members of TMNs and this is especially true of plants in less developed countries. In contrast, national climate policies are unrelated to plants’ environmental performance over time. Although our analyses suggest TMNs help to reduce the emissions of the typical power plant, they also indicate they have little bearing on the emissions of the world’s most egregious polluting plants.

 

Although the potential for cities and regions to contribute to global mitigation efforts is widely acknowledged, there is little evidence on the effectiveness of subnational mitigation strategies. Here we address this gap through a systematic review of 234 quantitative mitigation case studies. We use a meta-analytical approach to estimate expected greenhouse gas emissions reductions from 12 categories of mitigation strategies. We find that strategies related to land use and development, circular economy, and waste management are most effective and reliable for reducing emissions. The results demonstrate that cities and regions are taking widespread action to reduce emissions. However, we find misalignment between the strategies that policymakers and researchers focus on, compared to those with the highest expected impacts. The results inform climate action planning at the city and regional level and the evaluation of subnational climate targets.

 

Ecologists have put forward many explanations for coexistence, but these are onlypartial explanations; nature is complex, so it is reasonable to assume that in any given ecological community, multiple mechanisms of coexistence are operating at the same time. Here, we present a methodology for quantifying the relative importance of different explanations for coexistence, based on an extension of theModern Coexistence Theory. Current versions of Modern Coexistence Theory only allow for the analysis of communities that are affected by spatialortemporal environmental variation, but not both. We show how to analyze communities with spatiotemporal fluctuations, how to parse the importance of spatial variation and temporal variation, and how to measure everything with either mathematical expressions or simulation experiments. Our extension of Modern Coexistence Theory shows that many more species can coexist than originally thought. More importantly, it allows empiricists to use realistic models and more data to better infer the mechanisms of coexistence in real communities.

 

We introduce Hardware-assisted Fault Isolation (HFI), a simple extension to existing processors to support secure, flexible, and efficient in-process isolation. HFI addresses the limitations of existing software-based isolation (SFI) systems including: runtime overheads, limited scalability, vulnerability to Spectre attacks, and limited compatibility with existing code. HFI can seamlessly integrate with current SFI systems (e.g., WebAssembly), or directly sandbox unmodi!ed native binaries. To ease adoption, HFI relies only on incremental changes to the data and control path of existing high-performance processors. We evaluate HFI for x86-64 using the gem5 simulator and compiler-based emulation on a mix of real and synthetic workloads. 

Most programs compiled to WebAssembly (Wasm) today are written in unsafe languages like C and C++. Unfortunately, memory-unsafe C code remains unsafe when compiled to Wasm—and attackers can exploit buffer overflows and use-after-frees in Wasm almost as easily as they can on native platforms. Memory- Safe WebAssembly (MSWasm) proposes to extend Wasm with language-level memory-safety abstractions to precisely address this problem. In this paper, we build on the original MSWasm position paper to realize this vision. We give a precise and formal semantics of MSWasm, and prove that well-typed MSWasm programs are, by construction, robustly memory safe. To this end, we develop a novel, language-independent memory-safety property based on colored memory locations and pointers. This property also lets us reason about the security guarantees of a formal C-to-MSWasm compiler—and prove that it always produces memory-safe programs (and preserves the semantics of safe programs). We use these formal results to then guide several implementations: Two compilers of MSWasm to native code, and a C-to-MSWasm compiler (that extends Clang). Our MSWasm compilers support different enforcement mechanisms, allowing developers to make security-performance trade-offs according to their needs. Our evaluation shows that on the PolyBenchC suite, the overhead of enforcing memory safety in software ranges from 22% (enforcing spatial safety alone) to 198% (enforcing full memory safety), and 51.7% when using hardware memory capabilities for spatial safety and pointer integrity. More importantly, MSWasm’s design makes it easy to swap between enforcement mechanisms; as fast (especially hardware-based) enforcement techniques become available, MSWasm will be able to take advantage of these advances almost for free. 

Software sandboxing or software-based fault isolation (SFI) is a lightweight approach to building secure systems out of untrusted components. Mozilla, for example, uses SFI to harden the Firefox browser by sandboxing third-party libraries, and companies like Fastly and Cloudflare use SFI to safely co-locate untrusted tenants on their edge clouds. While there have been significant efforts to optimize and verify SFI enforcement, context switching in SFI systems remains largely unexplored: almost all SFI systems use heavyweight transitions that are not only error-prone but incur significant performance overhead from saving, clearing, and restoring registers when context switching. We identify a set of zero-cost conditions that characterize when sandboxed code has sufficient structured to guarantee security via lightweight zero-cost transitions (simple function calls). We modify the Lucet Wasm compiler and its runtime to use zero-cost transitions, eliminating the undue performance tax on systems that rely on Lucet for sandboxing (e.g., we speed up image and font rendering in Firefox by up to 29.7% and 10% respectively). To remove the Lucet compiler and its correct implementation of the Wasm specification from the trusted computing base, we (1) develop a static binary verifier , VeriZero, which (in seconds) checks that binaries produced by Lucet satisfy our zero-cost conditions, and (2) prove the soundness of VeriZero by developing a logical relation that captures when a compiled Wasm function is semantically well-behaved with respect to our zero-cost conditions. Finally, we show that our model is useful beyond Wasm by describing a new, purpose-built SFI system, SegmentZero32, that uses x86 segmentation and LLVM with mostly off-the-shelf passes to enforce our zero-cost conditions; our prototype performs on-par with the state-of-the-art Native Client SFI system. 

Unexpected population crashes are an important feature of natural systems, yet many observed crashes have not been explained. Two difficulties in explaining population crashes are their relative rarity and the multi‐causal nature of ecological systems. We approach this issue with experimental microcosms, with large numbers of replicates of red flour beetle populations (Tribolium castaneum). We determined that population crashes are caused by an interaction between stochasticity and successive episodes of density dependence: demographic stochasticity in oviposition rates occasionally produces a high density of eggs; so high that there are insufficient flour resources for subsequent larvae. This mechanism can explain unexpected population crashes in more general settings: stochasticity ‘pushes’ population into a regime where density dependence is severely overcompensatory. The interaction between nonlinearity and stochasticity also produces chaotic population dynamics and a double‐humped one‐generation population map, suggesting further possibilities for unexpected behaviour in a range of systems. We discuss the generality of our proposed mechanism, which could potentially account for previously inexplicable population crashes.

 

WebAssembly (Wasm) is a platform-independent bytecode that offers both good performance and runtime isolation. To implement isolation, the compiler inserts safety checks when it compiles Wasm to native machine code. While this approach is cheap, it also requires trust in the compiler's correctness---trust that the compiler has inserted each necessary check, correctly formed, in each proper place. Unfortunately, subtle bugs in the Wasm compiler can break---and have broken---isolation guarantees. To address this problem, we propose verifying memory isolation of Wasm binaries post-compilation. We implement this approach in VeriWasm, a static offline verifier for native x86-64 binaries compiled from Wasm; we prove the verifier's soundness, and find that it can detect bugs with no false positives. Finally, we describe our deployment of VeriWasm at Fastly.