Monday, August 24th, 2015

Time	Event
12:00a	Crash-tolerant data storage In a computer operating system, the file system is the part that writes data to disk and tracks where the data is stored. If the computer crashes while it’s writing data, the file system’s records can become corrupt. Hours of work could be lost, or programs could stop working properly. At the ACM Symposium on Operating Systems Principles in October, MIT researchers will present the first file system that is mathematically guaranteed not to lose track of data during crashes. Although the file system is slow by today’s standards, the techniques the researchers used to verify its performance can be extended to more sophisticated designs. Ultimately, formal verification could make it much easier to develop reliable, efficient file systems. “What many people worry about is building these file systems to be reliable, both when they’re operating normally but also in the case of crashes, power failure, software bugs, hardware errors, what have you,” says Nickolai Zeldovich, an associate professor of computer science and engineering and one of three MIT computer-science professors on the new paper. “Making sure that the file system can recover from a crash at any point is tricky because there are so many different places that you could crash. You literally have to consider every instruction or every disk operation and think, ‘Well, what if I crash now? What now? What now?’ And so empirically, people have found lots of bugs in file systems that have to do with crash recovery, and they keep finding them, even in very well tested file systems, because it’s just so hard to do.” Proving ground Zeldovich and his colleagues — Frans Kaashoek, the Charles A. Piper Professor in MIT’s Department of Electrical Engineering and Computer Science (EECS); associate professor of computer science Adam Chlipala; Haogang Chen, a graduate student in EECS; and Daniel Ziegler, an undergraduate in EECS — established the reliability of their file system through a process known as formal verification. Formal verification involves mathematically describing the acceptable bounds of operation for a computer program and then proving that the program will never exceed them. It’s a complicated process, so it’s generally applied only to very high-level schematic representations of a program’s functionality. Translating those high-level schema into working code, however, can introduce myriad complications that the proofs don’t address. “All these paper proofs about other file systems may actually be correct, but there’s no file system that we can be sure represents what the proof is about,” Ziegler says. What distinguishes the MIT researchers’ work is that they prove properties of the file system’s final code, not a high-level schema. To do that, they took advantage of a tool known as a proof assistant, which provides a formal language for describing aspects of a computer system and the relationships between them. “This formal proving environment includes a programming language,” Chlipala explains. “So we implement the file system in the same language where we’re writing the proofs. And the proofs are checked against the actual file system, not some whiteboard idealization that has no formal connection to the code.” The proof assistant, known as Coq, provided the tools, but the MIT researchers still had to do the work. First, they had to describe the components of a file system using Coq’s formal language. “You have to define, ‘What is a disk?’” Zeldovich says. “And ‘What is a bit?’” Chlipala adds. Next, they had to formally describe the relationships between the behaviors of these different components under crash conditions. Only then could they begin to construct a proof that a file system would behave the way it should. Finally, they had to write the corresponding file system. The part of the process that Coq automated was determining that the file system did, in fact, adhere to the logical relationships described in the proof. Reproducibility In the course of writing the file system, they repeatedly went back and retooled the system specifications, and vice versa. But even though they rewrote the file system “probably 10 times,” Zeldovich says, Kaashoek estimates that they spent 90 percent of their time on the definitions of the system components and the relationships between them and on the proof. “We’ve written file systems many times over, so we know exactly what it’s going to look like,” Zeldovich says. “Whereas with all these logics and proofs, there are so many ways to write them down, and each one of them has subtle implications down the line that we didn’t really understand.” “No one had done it,” Kaashoek adds. “It’s not like you could look up a paper that says, ‘This is the way to do it.’ But now you can read our paper and presumably do it a lot faster.” “It’s not like people haven’t proven things in the past,” says Ulfar Erlingsson, lead manager for security research at Google, who has observed the new work from a distance. “But usually the methods and technologies, the formalisms that were developed for creating the proofs, were so esoteric and so specific to the problem that there was basically hardly any chance that there would be repeat work that built up on it. But I can say for certain that Adam’s stuff with Coq, and separation logic, this is stuff that’s going to get built on and applied in many different domains. That’s what’s so exciting.” (Comment on this)
10:59a	Protein found to play a key role in blocking pathogen survival Invading microbial pathogens must scavenge essential nutrients from their host organism in order to survive and replicate. To defend themselves from infection, hosts attempt to block pathogens’ access to these nutrients. Now researchers at MIT have discovered the vital role a protein, calprotectin, plays in this process, known as “nutritional immunity.” In a paper published today in Nature Chemical Biology, the researchers describe the process by which human calprotectin prevents invading pathogens from obtaining iron, an extremely important nutrient. Transition metal ions, such as iron, zinc, and manganese, are essential for all organisms, according to Elizabeth Nolan, an associate professor of chemistry at MIT, who led the research. “What that means in the context of the host-pathogen interaction is that an invading microorganism needs to acquire these nutrient metal ions from the host,” Nolan says. “That is a challenge because the host tries to restrict metal-ion availability during infection, using a variety of strategies,” she says. Broad antimicrobial effects One such strategy is the use of proteins that chelate, or bind with metal ions, and so take them out of the pathogen’s reach. Previous research has identified that the protein calprotectin can sequester zinc and manganese. But while important, these nutrients alone do not fully explain the broad-spectrum antimicrobial effect that calprotectin is known to have, since different organisms have different metal-ion requirements, Nolan says. So Nolan and her colleagues began to investigate whether the protein is also capable of sequestering iron. The researchers first added calprotectin to a bacterial growth medium containing metal ions, to determine which metals it would bind to, and under what conditions. They found that the protein did indeed deplete the iron from the medium, and the presence of excess calcium in the medium resulted in substantially greater iron depletion. This calcium effect was in line with previous work by the researchers, which had shown that the protein “morphs” into a far more effective scavenger of zinc and manganese ions when calcium is present. “Calcium converts calprotectin into a form that more readily sequesters iron, so it binds to it with higher affinity,” Nolan says. Unlike when scavenging zinc and manganese, however, the researchers observed that the ability of calprotectin to sequester iron also depended on the presence of a reducing agent, beta-mercaptoethanol (BME).  This observation suggests that the protein has a preference for scavenging ferrous iron, or iron(II). That is because the reducing agent, BME, will keep iron in the iron(II) oxidation state. “We found there was approximately a 30-fold reduction in total iron in the medium, under the presence of calcium and BME,” Nolan says. “So this shows that calprotectin is very good at sequestering iron(II), and it does so in a way that’s dependent on the presence of calcium ions,” she says. Bacterial growth blocked The researchers then added bacteria to the calprotectin-treated medium, in a bid to determine what effect this reduction in iron concentration would have on the invading pathogens. They found that the growth of all the bacteria was inhibited by the lack of available iron. They then substituted metal ions back into the medium. They found that Gram-negative bacteria such as E. coli were only able to grow back once iron was added to the medium. Indeed, adding iron alone was enough for some Gram-negative bacteria to fully recover, Nolan says. In the case of Gram-positive bacteria such as Staphylococcus aureus, however, the microorganisms required mixtures of iron, manganese, and zinc to show maximum growth recovery, she says. “The data indicates that the ability of calprotectin to sequester iron has a significant impact on the growth of Gram-negative organisms,” Nolan says. “Iron sequestration also contributes to the growth inhibition of Gram-positive organisms, but we need to add more than just iron back in, in order for them to recover,” she says. When the researchers then added both calprotectin and bacteria to a growth medium containing the radioactive isotope iron-55, they were able to observe that the presence of the protein prevented the microorganisms from acquiring the metal. Finally, the researchers performed biochemical and spectroscopic analysis — the latter in collaboration with Carsten Krebs, a professor of chemistry, biochemistry, and molecular biology at Penn State University — to characterize the iron(II) binding site of calprotectin. They found that calprotectin uses an unusual hexahistidine motif to bind iron(II). The research suggests a model by which calprotectin, which is housed in the cytoplasm of a cell, uses changes in calcium concentration to tune its metal-sequestering function, Nolan says. “Under resting conditions calcium ion concentrations are low [within the cytoplasm], but then when calprotectin is released into the extracellular space at the site of an infection, the concentration of calcium is orders of magnitude higher,” she says. “Calprotectin then binds to calcium and converts to its high-affinity form, and that allows it to sequester metals from microbes.” The research could contribute to efforts to develop methods to boost the immune system’s metal ion withholding response, and thereby fight bacterial infection, Nolan says. This study highlights the versatility of calprotectin, according to David Giedroc, a professor of chemistry at Indiana University who was not involved in the research. “Calprotectin is exclusively regarded by the community as a calcium-activated manganese- and zinc-binding protein, and all the physiological effects of calprotectin in nutritional immunity have previously been attributed to the withholding of these two important transition metal ions only,” Giedroc says. “This new work establishes clearly, for the first time, that [calprotectin] has the ability to bind iron(II), and this activity appears to be important for inhibition of growth of a wide range of bacterial pathogens,” he says. (Comment on this)
8:00p	Study identifies new cheating method in MOOCs While the proliferation of massive open online courses (MOOCs) has expanded learning opportunities for individuals around the world, the digital classroom is also subject to many of the same issues as the traditional one, such as cheating. In a new working paper, researchers at MIT and Harvard University identify a new method of cheating specific to open online courses and recommend a number of strategies that prove effective in preventing such cheating. The working paper, “Detecting and Preventing ‘Multiple-Account’ Cheating in Massive Open Online Courses,” was published today on arXiv.org, an online repository for electronic preprints. Isaac Chuang — a professor of electrical engineering and physics, senior associate dean of digital learning at MIT, and one of the authors of the working paper — explains that he and his colleagues were inspired to examine the problem in an effort to better understand all the opportunities that online courses provide, including both learning and cheating. “If learners in some online courses are circumventing the learning process and obtaining certification without going through the traditional routes of assessment and feedback, then the certification does not necessarily imply that they learned anything. This could seriously devalue MOOC certification,” Chuang says. “This is a well-known issue in academics, and it’s happening in a new ways in online settings. We want to understand and address this issue as online education continues to grow.” Andrew Ho, a professor at the Harvard Graduate School of Education and an author of the working paper, adds that the paper describes “a new cheating technique that is particular to MOOCs. It is enabled by specific design features, including the ability to create multiple accounts for free. This is a method of cheating that allows you to acquire a certification for a course in an hour, which is not possible through conventional cheating approaches. This is cheating of a different kind.” CAMEO users While analyzing data gathered from learners using the edX online learning platform, the researchers noticed that certain users were answering assessment questions “faster than is humanly possible,” according to Chuang. Upon further examination, the researchers realized that a number of learners appeared to be employing a cheating strategy they refer to as “copying answers using multiple existences online” (or CAMEO). In this method of cheating, a user creates multiple accounts, one of which is the primary account that will ultimately earn a certificate. The other accounts are used to find or “harvest” the correct answers to assessment questions for the master account.  To determine the amount of cheating occurring in classes where learners can obtain certification for passing the course, the researchers developed a new algorithm that can identify CAMEO users. The algorithm searches for pairs of related accounts in which one account responds to most of the answers incorrectly and the other provides mostly correct answers on the first attempt. Activity time stamps are then reviewed to see when the account suspected of harvesting answers solved a particular problem just after the master account did. The algorithm also looks to see whether related accounts might share IP addresses across multiple courses. The researchers examined data gathered from 1.9 million course participants in 115 MOOCs offered by HarvardX and MITx from the fall of 2012 through the spring of 2015. They discovered that in 69 courses where users were found to have been employing the CAMEO strategy, 1.3 percent of the certificates earned (1,237 certificates) appeared to have been obtained through such cheating. Additionally, they found that among earners of 20 or more certificates, 25 percent appear to have used the CAMEO strategy. In some courses CAMEO users may account for as many as 5 percent of certificates earned. Although these percentages are lower than the prevalence of reported cheating, which by some accounts is greater than 50 percent, the authors argue that these percentages are nonetheless significant. “This is not an isolated incident of copying on part of one assignment,” Ho says. “This is the wholesale falsification of a certificate.” CAMEO usage was found to be higher among young, less-educated males outside the United States. The rate among users from the United States was particularly low, at 0.4 percent of certificates earned. The authors observe that these rates may correlate with the perceived value of the certificate across different countries. The prevalence of CAMEO usage was highest in government, health, and social science courses, where 1.3 percent of certificates were earned by employing the CAMEO strategy, and lowest in computer science courses, where just 0.1 percent of certificates were obtained using the technique. Prevention techniques The authors outline a number of strategies to prevent cheating in online courses, including restricting solutions to assessments until after assignments are due, and randomizing questions so that each learner receives a customized set of problems. However, some of these strategies are costly or may limit learning opportunities. “We may face a tradeoff between enabling learning and preventing cheating,” Chuang notes. The researchers found that in the science, technology, engineering, and mathematics (STEM) courses where such techniques may have been employed, CAMEO usage accounted for just 0.1 percent of certificates earned, as opposed to 1.2 percent of certificates earned in courses that did not use any prevention strategies. While techniques including randomization are easy to employ in STEM courses, Chuang notes that they are more challenging to implement in humanities courses, where multiple-choice questions are commonly used as part of the assessment process. Nonetheless, the researchers are hopeful that their findings will inspire course content creators to implement some of the prevention strategies they have outlined and that this research will inspire further evaluation of cheating in MOOCs. “One of the most interesting lessons from the paper is that there are ways to mitigate cheating that are straightforward and implementable by the teams creating online course content,” Chuang explains. “We also expect platform improvements, such as virtual proctoring, to help reduce cheating.” “This paper addresses a growing challenge as higher education digitizes: ensuring that the work that students do is their work,” says George Siemens, executive director of the Learning Innovation and Networked Knowledge research lab at the University of Texas at Arlington, who was not involved in the research. “MOOCs, and in the case of this paper, the development of multiple online identities, present a new set of challenges for academics,” Siemens says. “The stakes in learning can be high since academic performance can influence job opportunities. Ensuring that work is done by the student proclaiming to have done it will continue to be a challenge online and in classrooms.” (Comment on this)
11:59p	Paul O’Gorman: Extreme storm modeler Several winters back, while shoveling out his driveway after a particularly heavy snowstorm, Paul O’Gorman couldn’t help but wonder: How is climate change affecting the Boston region’s biggest snow events? The question wasn’t an idle one for O’Gorman: For the past decade, he’s been investigating how a warming climate may change the intensity and frequency of the world’s most extreme storms and precipitation events. In 2014, O’Gorman decided to look into how increased warming may affect daily snowfall around the world. In a Nature study that has since been widely quoted, he reported that while most of the Northern Hemisphere will see less total snowfall in a warmer climate, regions where the average winter temperature is near a “sweet spot” will still experience severe blizzards that dump over a foot of snow in a single day. As it happened, the following winter in Boston produced consecutive blizzards that covered the city in a record-breaking 110 inches of snow, with much of it falling in a single month. O’Gorman was on sabbatical in Australia at the time, and missed the towering snowbanks, damaging ice dams, and citywide gridlock. But Boston’s extreme winter has spurred a follow-on project for O’Gorman, who recently was awarded tenure as associate professor in MIT’s Department of Earth, Atmospheric and Planetary Sciences (EAPS). “While I have previously studied daily snowfall, it would definitely be interesting to study these extreme monthly snowfalls,” O’Gorman says. “They obviously can have a big impact in an urban environment, as we saw in Boston.” “Cross-fertilization of ideas” O’Gorman grew up in Tullamore, a small town in the midlands of Ireland that, like the rest of the country, receives frequent rainfall throughout the year, but seldom experiences very heavy rainfall or snowfall. Extreme precipitation was far from O’Gorman’s focus when he enrolled at Trinity College in Dublin. There, he chose to study theoretical physics, and later fluid dynamics, which gave him the opportunity to work with supercomputers to simulate fluid flow — work that earned him a master’s degree in high-performance computing. At the time, O’Gorman was interested in applying his work in fluid dynamics to problems related to turbulence generated by aircraft. In 1999, he headed to the United States, where he pursued a PhD in aeronautics at Caltech. “That was a bit of a jump culturally, for sure,” O’Gorman recalls. “One of the nice things is, Caltech is kind of a small place where, like MIT, there’s a lot of cross-fertilization of ideas.” In fact, O’Gorman’s interest in atmospheric science grew out of just such an opportunity. As part of his studies in aeronautical engineering, he took an elective on turbulence in the atmosphere and ocean, taught by climate scientist Tapio Schneider. “[The class] totally changed the course of my career and interests,” O’Gorman says. “I had been studying turbulence on small scales, and now I was learning about turbulence at the planetary scale. What struck me about the fluid flow of the atmosphere was that there are different layers, as well as the rotation of the planet, clouds, precipitation, and radiation all interacting at the same time, and there were a lot of unanswered questions that, to me, were all pretty fascinating.” After earning a PhD in aeronautics, O’Gorman switched career paths, and worked with Schneider as a postdoc, investigating turbulence in the atmosphere — and in particular, the atmosphere’s response to global warming. When Schneider was invited to a scientific meeting on extreme events, O’Gorman began a research project that ultimately set his course on the study of extreme precipitation. Climate shift In 2008, O’Gorman joined the EAPS faculty as an assistant professor, and has since been exploring the relationship between atmospheric warming and the atmospheric circulation and extreme events. Part of his research continues the work he did as a postdoc with Schneider, in which the two studied climate change’s effect on water vapor: As the climate warms, there is more water vapor in the atmosphere, which in turn acts to further heat the atmosphere. The effect of water vapor and latent heat release has not yet been fully incorporated in existing theories of the atmosphere. O’Gorman says understanding water vapor’s role could help explain how climate change affects rapidly deepening storms at mid-latitude locations, such as the United States and Europe. While much of his work is based on theoretical modeling, O’Gorman occasionally works with actual weather observations. In 2013, he looked to data collected by weather balloons around the world to see how the atmosphere’s temperature varies with altitude in recent decades. There exists a temperature gradient in the lowest layer of the atmosphere, in which temperatures get colder with altitude. O’Gorman and his student Martin Singh had predicted that as the climate warms, this gradient will essentially shift upward. However, the theory hadn’t been tested with observations. O’Gorman and Singh analyzed data from weather balloons around the world, each of which took temperature measurements as it rose up through the atmosphere. They found that, based on the measurements, the atmosphere’s temperature profile did indeed seem to be shifting upward over time, consistent with the theory. “We found if you look at the temperature profile in the current climate, you can predict what it will do in a warmer climate,” O’Gorman says. “This is one of the factors that affects how much radiation is emitted to space, which affects how much the planet warms.” In the next few years, he hopes to take advantage of the increasing computing power of climate models to track the intensity of rain and snowstorms in response to influences such as greenhouse gases. “Computers have gotten powerful enough now that we can do simulations of the whole globe, while resolving clouds to some extent,” O’Gorman says. “We can study how convection organizes itself on all sorts of different scales, all the way up to planetary scales. So I think this is a very exciting moment.” (Comment on this)

<< Previous Day

2015/08/24 [Calendar]

Next Day >>