Tanshinone ⅡA prevents acute lung injury by regulating macrophage polarization

Objective: Acute lung injury(ALI) is a serious respiratory dysfunction caused by pathogen or physical invasion. The strong induced inflammation often causes death. Tanshinone ⅡA(Tan-ⅡA) is the major constituent of Salvia miltiorrhiza Bunge and has been shown to display anti-inflammatory effects. The aim of the current study was to investigate the effects of Tan-ⅡA on ALI.Methods: A murine model of lipopolysaccharide(LPS)-induced ALI was used. The lungs and serum samples of mice were extracted at 3 days after treatment. ALI-induced inflammatory damages were confirmed from cytokine detections and histomorphology observations. Effects of Tan-ⅡA were investigated using in vivo and in vitro ALI models. Tan-ⅡA mechanisms were investigated by performing Western blot and flow cytometry experiments. A wound-healing assay was performed to confirm the Tan-ⅡA function.Results: The cytokine storm induced by LPS treatment was detected at 3 days after LPS treatment, and alveolar epithelial damage and lymphocyte aggregation were observed. Tan-ⅡA treatment attenuated the LPS-induced inflammation and reduced the levels of inflammatory cytokines released not only by inhibiting neutrophils, but also by macrophage. Moreover, we found that macrophage activation and polarization after LPS treatment were abrogated after applying the Tan-ⅡA treatment. An in vitro assay also confirmed that including the Tan-ⅡA supplement increased the relative amount of the M2 subtype and decreased that of M1. Rebalanced macrophages and Tan-ⅡA inhibited activations of the nuclear factor-κB and hypoxia-inducible factor pathways. Including Tan-ⅡA and macrophages also improved alveolar epithelial repair by regulating macrophage polarization.Conclusion: This study found that while an LPS-induced cytokine storm exacerbated ALI, including Tan-ⅡA could prevent ALI-induced inflammation and improve the alveolar epithelial repair, and do so by regulating macrophage polarization.

A Lightweight Dynamic Enforcement of Privacy Protection for Android

Inter-process communication(IPC)provides a message passing mechanism for information exchange between applications.It has been long believed that IPCs can be abused by malware writers to launch collusive information leak using two or more applications.Much work on privacy protection focuses on the simple information leak caused by the individual applications and lacks effective approaches to preventing the collusive information leak caused by IPCs between multiple processes.In this paper,we propose a hybrid approach to prevent the collusive information leak based on information flow control.Our approach combines static information flow analysis and dynamic runtime checking together.Information leak caused by individual processes is prevented through static information flow control,and dynamic checking is done at runtime to prevent the collusive information leak.Such a combination may effectively reduce the runtime overhead of pure dynamic checking,and reduce false-alarms in pure static analysis.We develop this approach based on an abstract and simplified programming model,and formalize a novel definition of the leak-freedom property as our target security property.A simulation-based proof technique is used to prove that our approach is able to guarantee leak-freedom.All proofs are mechanized in Coq.

Verifying Contextual Refinement with Ownership Transfer

Contextual refinement is a compositional approach to compositional verification of concurrent objects.There has been much work designing program logics to prove the contextual refinement between the object implementation and its abstract specification.However,these program logics for contextual refinement verification cannot support objects with resource ownership transfer,which is a common pattern in many concurrent objects,such as the memory management module in OS kernels,which transfers the allocated memory block between the object and clients.In this paper,we propose a new approach to give abstract and implementation independent specifications to concurrent objects with ownership transfer.We also design a program logic to verify contextual refinement of concurrent objects w.r.t.their abstract specifications.We have successfully applied our logic to verifying an implementation of the memory management module,where the implementation is an appropriately simplified version of the original version from a real-world preemptive OS kernel.

Modular Verification of SPARCv8 Code

Inline assembly code is common in system software to interact with the underlying hardware platforms. The safety and correctness of the assembly code is crucial to guarantee the safety of the whole system. In this paper, we propose a practical Hoare-style program logic for verifying SPARC (Scalable Processor Architecture) assembly code. The logic supports modular reasoning about the main features of SPARCv8 ISA (instruction set architecture), including delayed control transfers, delayed writes to special registers, and register windows. It also supports relational reasoning for refinement verification. We have applied it to verify that there is a contextual refinement between a context switch routine in SPARCv8 and a switch primitive. The program logic and its soundness proof have been mechanized in Coq.