Secure information flow via stripping and fast simulation

Type systems for secure information flow aim to prevent a program from leaking information from H (high) to L (low) variables. Traditionally, bisimulation has been the prevalent technique for proving the soundness of such systems. This work introduces a new proof technique based on stripping and fast simulation, and shows that it can be applied in a number of cases where bisimulation fails. We present a progressive development of this technique over a representative sample of languages including a simple imperative language (core theory), a multiprocessing nondeterministic language, a probabilistic language, and a language with cryptographic primitives. In the core theory we illustrate the key concepts of this technique in a basic setting. A fast low simulation in the context of transition systems is a binary relation where simulating states can match the moves of simulated states while maintaining the equivalence of low variables; stripping is a function that removes high commands from programs. We show that we can prove secure information flow by arguing that the stripping relation is a fast low simulation. We then extend the core theory to an abstract distributed language under a nondeterministic scheduler. Next, we extend to a probabilistic language with a random assignment command; we generalize fast simulation to the setting of discrete time Markov Chains, and prove approximate probabilistic noninterference. Finally, we introduce cryptographic primitives into the probabilistic language and prove computational noninterference, provided that the underling encryption scheme is secure.

Importance of storm events in controlling ecosystem structure and function in a Florida gulf coast estuary

From 8/95 to 2/01, we investigated the ecological effects of intra- and inter-annual variability in freshwater flow through Taylor Creek in southeastern Everglades National Park. Continuous monitoring and intensive sampling studies overlapped with an array of pulsed weather events that impacted physical, chemical, and biological attributes of this region. We quantified the effects of three events representing a range of characteristics (duration, amount of precipitation, storm intensity, wind direction) on the hydraulic connectivity, nutrient and sediment dynamics, and vegetation structure of the SE Everglades estuarine ecotone. These events included a strong winter storm in November 1996, Tropical Storm Harvey in September 1999, and Hurricane Irene in October 1999. Continuous hydrologic and daily water sample data were used to examine the effects of these events on the physical forcing and quality of water in Taylor Creek. A high resolution, flow-through sampling and mapping approach was used to characterize water quality in the adjacent bay. To understand the effects of these events on vegetation communities, we measured mangrove litter production and estimated seagrass cover in the bay at monthly intervals. We also quantified sediment deposition associated with Hurricane Irene's flood surge along the Buttonwood Ridge. These three events resulted in dramatic changes in surface water movement and chemistry in Taylor Creek and adjacent regions of Florida Bay as well as increased mangrove litterfall and flood surge scouring of seagrass beds. Up to 5 cm of bay-derived mud was deposited along the ridge adjacent to the creek in this single pulsed event. These short-term events can account for a substantial proportion of the annual flux of freshwater and materials between the mangrove zone and Florida Bay. Our findings shed light on the capacity of these storm events, especially when in succession, to have far reaching and long lasting effects on coastal ecosystems such as the estuarine ecotone of the SE Everglades.

Nonlinear Flow in Karst Formations

The variation of effective hydraulic conductivity as a function of specific discharge in several 0.2-m and 0.3-m cubes of Key Largo Limestone was investigated. The experimental results closely match the Forchheimer equation. Defining the pore-size length scale in terms of Forchheimer parameters, it is demonstrated that significant deviations from Darcian flow will occur when the Reynolds number exceeds 0.11. A particular threshold model previously proposed for use in karstic formations does not show strong agreement with the data near the onset of nonlinear flow.

A tidal creek water budget: Estimation of groundwater discharge and overland flow using hydrologic modeling in the Southern Everglades

Taylor Slough is one of the natural freshwater contributors to Florida Bay through a network of microtidal creeks crossing the Everglades Mangrove Ecotone Region (EMER). The EMER ecological function is critical since it mediates freshwater and nutrient inputs and controls the water quality in Eastern Florida Bay. Furthermore, this region is vulnerable to changing hydrodynamics and nutrient loadings as a result of upstream freshwater management practices proposed by the Comprehensive Everglades Restoration Program (CERP), currently the largest wetland restoration project in the USA. Despite the hydrological importance of Taylor Slough in the water budget of Florida Bay, there are no fine scale (∼1 km2) hydrodynamic models of this system that can be utilized as a tool to evaluate potential changes in water flow, salinity, and water quality. Taylor River is one of the major creeks draining Taylor Slough freshwater into Florida Bay. We performed a water budget analysis for the Taylor River area, based on long-term hydrologic data (1999–2007) and supplemented by hydrodynamic modeling using a MIKE FLOOD (DHI,http://dhigroup.com/) model to evaluate groundwater and overland water discharges. The seasonal hydrologic characteristics are very distinctive (average Taylor River wet vs. dry season outflow was 6 to 1 during 1999–2006) with a pronounced interannual variability of flow. The water budget shows a net dominance of through flow in the tidal mixing zone, while local precipitation and evapotranspiration play only a secondary role, at least in the wet season. During the dry season, the tidal flood reaches the upstream boundary of the study area during approximately 80 days per year on average. The groundwater field measurements indicate a mostly upwards-oriented leakage, which possibly equals the evapotranspiration term. The model results suggest a high importance of groundwater contribution to the water salinity in the EMER. The model performance is satisfactory during the dry season where surface flow in the area is confined to the Taylor River channel. The model also provided guidance on the importance of capturing the overland flow component, which enters the area as sheet flow during the rainy season. Overall, the modeling approach is suitable to reach better understanding of the water budget in the mangrove region. However, more detailed field data is needed to ascertain model predictions by further calibrating overland flow parameters.