Search for: All records

We present Mohabi—a modern Firefox browser with a securely sandboxed JavaScript engine. Mohabi leverages software-based fault isolation (SFI) to ensure JavaScript engine bugs cannot affect the rest of the browser. To achieve this, we disaggregated the JavaScript engine (SpiderMonkey) from the rest of the browser, and developed techniques that leverage the type system and automatic code generation to make this complex transformation—that spans numerous data structures and deeply intertwined control flow across tens of thousands of functions—safe and tractable with reasonable engineering effort. We then sandboxed SpiderMonkey using an optimized SFI toolchain we developed to meet the unique challenges of JavaScript engines, such as efficient support for large memory footprints. Mohabi only incurs modest overheads on common benchmarks—24.82% on JetStream and 24.43% on Speedometer. Mohabi is the most ambitious case study in retrofitting in-process sandboxing in a large system to date, and our x86-64 SFI toolchain is the fastest to date, imposing overheads between 5.9%–6.6% in SPEC 2017. 

LLMs’ remarkable ability to tackle a wide range of language tasks opened new opportunities for collaborative human-AI problem solving. LLMs can amplify human capabilities by applying their intuitions and reasoning strategies at scale. We explore whether human guides can be simulated, by generalizing from human demonstrations of guiding an AI system to solve complex language problems. We introduce CoLa, a novel self-guided learning paradigm for training automated guides and evaluate it on two QA datasets, a puzzle-solving task, and a constrained text generation task. Our empirical results show that CoLa consistently outperforms competitive approaches across all domains. Moreover, a small-sized trained guide outperforms a strong model like GPT-4 when acting as a guide. We compare the strategies employed by humans and automated guides by conducting a human study on a QA dataset. We show that automated guides outperform humans by adapting their strategies to reasoners’ capabilities and conduct qualitative analyses highlighting distinct differences in guiding strategies 

Abstract Structural and mechanical cues from the extracellular matrix (ECM) regulate tissue morphogenesis. Tissue development has conventionally been studied withex vivosystems where mechanical properties of the extracellular environment are either poorly controlled in space and time, lack tunability, or do not mimic ECM mechanics. For these reasons, it remains unknown how matrix stress relaxation rate, a time-dependent mechanical property that influences several cellular processes, regulates mammary branching morphogenesis. Here, we systematically investigated the influence of matrix stress relaxation on mammary branching morphogenesis using 3D alginate-collagen matrices and spheroids of human mammary epithelial cells. Slow stress relaxing matrices promoted significantly greater branch formation compared to fast stress relaxing matrices. Branching in slow stress relaxing matrices was accompanied by local collagen fiber alignment, while collagen fibers remained randomly oriented in fast stress relaxing matrices. In slow stress relaxing matrices, branch formation was driven by intermittent pulling contractions applied to the local ECM at the tips of elongating branches, which was accompanied by an abundance of phosphorylated focal adhesion kinase (phospho-FAK) and β1 integrin at the tips of branches. On the contrary, we observed that growing spheroids in fast stress relaxing matrices applied isotropic pushing forces to the ECM. Pharmacological inhibition of both Rac1 and non-muscle myosin II prevented epithelial branch formation, regardless of matrix stress relaxation rate. Interestingly, restricting cellular expansion via increased osmotic pressure was sufficient to impede epithelial branching in slow stress relaxing matrices. This work highlights the importance of stress relaxation in regulating and directing mammary branch elongation. 

Abstract Reconstituted basement membrane (rBM) products like Matrigel are widely used in 3D culture models of epithelial tissues and cancer. However, their utility is hindered by key limitations, including batch variability, xenogenic contaminants, and a lack of tunability. To address these challenges, we engineered a 3D basement membrane (eBM) matrix by conjugating defined extracellular matrix (ECM) adhesion peptides (IKVAV, YIGSR, RGD) to an alginate hydrogel network with precisely tunable stiffness and viscoelasticity. We optimized the mechanical and biochemical properties of the engineered basement membranes (eBMs) to support mammary acinar morphogenesis in MCF10A cells, similar to rBM. We found that IKVAV-modified, fast-relaxing (τ_1/2= 30-150 s), and soft (E = 200 Pa) eBMs best promoted polarized acinar structures. Clusters became invasive and lost polarity only when the IKVAV-modified eBM exhibited both similar stiffness to a malignant breast tumor (E = 4000 Pa) and slow stress relaxation (τ_1/2= 600-1100 s). Notably, tumor-like stiffness alone was not sufficient to drive invasion in fast stress relaxing matrices modified with IKVAV. In contrast, RGD-modified matrices promoted a malignant phenotype regardless of mechanical properties. We also utilized this system to interrogate the mechanism driving acinar and tumorigenic phenotypes in response to microenvironmental parameters. A balance in activity between β1- and β4-integrins was observed in the context of IKVAV-modified eBMs, prompting further investigation into the downstream mechanisms. We found differences in hemidesmosome formation and production of endogenous laminin in response to peptide type, stress relaxation, and stiffness. We also saw that inhibiting either focal adhesion kinase or hemidesmosome signaling in IKVAV eBMs prevented acinus formation. This eBM matrix is a powerful, reductionist, xenogenic-free system, offering a robust platform for both fundamental research and translational applications in tissue engineering and disease modeling. 

Abstract Breast cancer progression is marked by extracellular matrix (ECM) remodeling, including increased stiffness, faster stress relaxation, and elevated collagen levels. In vitro experiments have revealed a role for each of these factors to individually promote malignant behavior, but their combined effects remain unclear. To address this, we developed alginate-collagen hydrogels with independently tunable stiffness, stress relaxation, and collagen density. We show that these combined tumor-mimicking ECM cues reinforced invasive morphologies and promoted spheroid invasion in breast cancer and mammary epithelial cells. High stiffness and low collagen density in slow-relaxing matrices led to the greatest cell migration speed and displacement. RNA-seq revealed Sp1 target gene enrichment in response to both individual and combined ECM cues, with a greater enrichment observed under multiple cues. Notably, high expression of Sp1 target genes upregulated by fast stress relaxation correlated with poor patient survival. Mechanistically, we found that phosphorylated-Sp1 (T453) was increasingly located in the nucleus in stiff and/or fast relaxing matrices, which was regulated by PI3K and ERK1/2 signaling, as well as actomyosin contractility. This study emphasizes how multiple ECM cues in complex microenvironments reinforce malignant traits and supports an emerging role for Sp1 as a mechanoresponsive transcription factor. 

Upon osmotic compression, rotationally symmetric faceted colloidal particles can form translationally ordered, orientationally disordered rotator mesophases. This study explores the mechanism of rotator-to-crystal phase transitions where orientational order is gained in a translationally ordered phase, using rotator-phase forming truncated cubes as a testbed. Monte Carlo simulations were conducted for two selected truncations (s), one for s = 0.527 where the rotator and crystal lattices are dissimilar and one for s = 0.572 where the two phases have identical lattices. These differences set the stage for a qualitative difference in their rotator–crystal transitions, highlighting the effect of lattice distortion on phase transition kinetics. Our simulations reveal that significant lattice deviatoric effects could hinder the rotator-to-crystal transition and favor arrangements of lower packing fraction instead. Indeed, upon compression, it is found that for s = 0.527, the rotator phase does not spontaneously transition into the stable, densely packed crystal due to the high lattice strains involved but instead transitions into a metastable solid phase to be colloquially referred to as “orientational salt” for short, which has a similar lattice as the rotator phase and exhibits two distinct particle orientations having substitutional order, alternating regularly throughout the system. This study paves the way for further analysis of diffusionless transformations in nanoparticle systems and how lattice-distortion could influence crystallization kinetics. 

Just-in-time (JIT) compilers make JavaScript run efficiently by replacing slow JavaScript interpreter code with fast machine code. However, this efficiency comes at a cost: bugs in JIT compilers can completely subvert all language-based (memory) safety guarantees, and thereby introduce catastrophic exploitable vulnerabilities. We present Icarus: a new framework for implementing JIT compilers that are automatically, formally verified to be safe, and which can then be converted to C++ that can be linked into browser runtimes. Crucially, we show how to build a JIT with Icarus such that verifying the JIT implementation statically ensures the security of all possible programs that the JIT could ever generate at run-time, via a novel technique called symbolic meta-execution that encodes the behaviors of all possible JIT-generated programs as a single Boogie meta-program which can be efficiently verified by SMT solvers. We evaluate Icarus by using it to re-implement components of Firefox's JavaScript JIT. We show that Icarus can scale up to expressing complex JITs, quickly detects real-world JIT bugs and verifies fixed versions, and yields C++ code that is as fast as hand-written code.