Large language models (LLMs) trained on general domain corpora showed remarkable results on natural language processing (NLP) tasks. However, previous research demonstrated LLMs trained using domain-focused corpora perform better on specialized tasks. Inspired by this insight, we developed INDUS, a comprehensive suite of LLMs tailored for the closely-related domains of Earth science, biology, physics, heliophysics, planetary sciences and astrophysics, and trained using curated scientific corpora drawn from diverse data sources. The suite of models include: (1) an encoder model trained using domain-specific vocabulary and corpora to address NLP tasks, (2) a contrastive-learning based text embedding model trained using a diverse set of datasets to address information retrieval tasks and (3) smaller versions of these models created using knowledge distillation for applications which have latency or resource constraints. We also created three new scientific benchmark datasets, Climate-Change NER (entity-recognition), NASA-QA (extractive QA) and NASA-IR (IR) to accelerate research in these multi-disciplinary fields. We show that our models outperform both general-purpose (RoBERTa) and domain- specific (SciBERT) encoders on these new tasks as well as existing tasks in the domains of interest. Furthermore, we demonstrate the use of these models in two industrial settings- as a retrieval model for large-scale vector search applications and in automatic content tagging systems.

Accurate document layout analysis is a key requirement for high-quality PDF document conversion. With the recent availability of public, large ground-truth datasets such as PubLayNet and DocBank, deep-learning models have proven to be very effective at layout detection and segmentation. While these datasets are of adequate size to train such models, they severely lack in layout variability since they are sourced from scientific article repositories such as PubMed and arXiv only. Consequently, the accuracy of the layout segmentation drops significantly when these models are applied on more challenging and diverse layouts. In this paper, we present DocLayNet, a new, publicly available, document-layout annotation dataset in COCO format. It contains 80863 manually annotated pages from diverse data sources to represent a wide variability in layouts. For each PDF page, the layout annotations provide labelled bounding-boxes with a choice of 11 distinct classes. DocLayNet also provides a subset of double- and triple-annotated pages to determine the inter-annotator agreement. In multiple experiments, we provide baseline accuracy scores (in mAP) for a set of popular object detection models. We also demonstrate that these models fall approximately 10% behind the inter-annotator agreement. Furthermore, we provide evidence that DocLayNet is of sufficient size. Lastly, we compare models trained on PubLayNet, DocBank and DocLayNet, showing that layout predictions of the DocLayNet-trained models are more robust and thus the preferred choice for general-purpose document-layout analysis.

In this paper, we present IBM's cognitive strategy for service delivery transformation to a services integration approach for IT service management. This transformation is fueled by three fundamental technological paradigms: cognitive, cloud, and data and digital content. At the foundation of this approach is the IBM Services Platform with Watson-an IBM Cloud and Watson-based platform that uses machine learning, natural language, discovery, and various Watson application programming interfaces to design superior client solutions, achieve an exceptional level of autonomic service management, and facilitate a healthy "always-on" environment. It continuously learns and optimizes information technology performance to enable enhanced client business outcomes.

It is a challenge to migrate and transform existing workloads into the cloud, especially those requiring the higher standardization of managed services. Covered here are the various types of transition and transformation into the cloud from lift and shift to automated migration; the tooling and automation for the cloud environment; and the migration services via wave planning and check-pointing to the cloud for customers. Transition and Transformation is an integral part of cloud services, and creating a repeatable, reusable, factory model for a customer ensures a successful cloud migration.

Web services are an important series of industry standards for adding semantics to web-based and XML-based communication, in particular among enterprises. Like the entire series, the security standards and proposals are highly modular. Combinations of several standards are put together for testing as interoperability scenarios, and these scenarios are likely to evolve into industry best practices. In the terminology of security research, the interoperability scenarios correspond to security protocols. Hence, it is desirable to analyze them for security. In this paper, we analyze the security of the new Secure WS-ReliableMessaging Scenario, the first scenario to combine security elements with elements of another quality-of-service standard. We do this both symbolically and cryptographically. The results of both analyses are positive. The discussion of actual cryptographic primitives of web services security is a novelty of independent interest in this paper.

We present the first idealized cryptographic library that ca n be used like the Dolev-Yao model for automated proofs of cryptograp hic protocols that use nested cryptographic operations, while coming with a cr yptographic implementation that is provably secure under active attacks. To illustrate the usefulness of the cryptographic library, we present a cryptographically sound security proof of the well-known Needham-Schr oeder-Lowe publickey protocol for entity authentication. This protocol was p reviously only proved over unfounded abstractions from cryptography. We show tha t the protocol is secure against arbitrary active attacks if it is implemented u sing standard provably secure cryptographic primitives. Conducting the proof by m eans of the idealized cryptographic library does not require us to deal with the pr obabilistic aspects of cryptography, hence the proof is in the scope of current auto ma ed proof tools. Besides establishing the cryptographic security of the Nee dham-Schroeder-Lowe protocol, this exemplifies the potential of this cryptograp hic library and paves the way for the cryptographically sound verification of securit y protocols by auto-

Symbolic secrecy of exchanged keys is arguably one of the mos t i portant notions of secrecy shown with automated proof tools. It means that an adversary restr icted to symbolic operations on terms can never get the entire key into its knowledge set. Cryptograph ic key secrecy essentially means computational indistinguishability between the real key and a rand om one, given the view of a much more general adversary. We provide the first proof of cryptographic key secrecy for th e strengthened Yahalom protocol, which constitutes one of the most prominent key exchange protocol s analyzed by means of automated proof tools. The proof holds in the presence of arbitrary active at tacks provided that the protocol is implemented using standard provably secure cryptographic primi tives. We exploit recent results on linking symbolic and cryptographic key secrecy in order to perform a symbolic proof of secrecy for the Yahalom protocol in a specific setting that allows us to derive t he desired cryptographic key secrecy from the symbolic proof.

We present a cryptographically sound security proof of the well-known NeedhamSchroeder-Lowe public-key protocol for entity authentication. This protocol was previously only proved over unfounded abstractions from cryptography. We show that it is secure against arbitrary active attacks if it is implemented using standard provably secure cryptographic primitives. Nevertheless, our proof does not have to deal with the probabilistic aspects of cryptography and is hence in the scope of current automated proof tools. We achieve this by exploiting a recently proposed Dolev-Yao-style cryptographic library with a provably secure cryptographic implementation. Besides establishing the cryptographic security of the Needham-Schroeder-Lowe protocol, our result exemplifies the potential of this cryptographic library and paves the way for the cryptographically sound verification of security protocols by automated proof tools.

We investigate how formal methods can be used for the verifica tion of cryptographic protocols such that the verified properties are valid for the concrete i mplementation of the protocol using actual cryptography. We give an abstract deterministic specificat on for secure message transmission with ordered channels along with a possible implementation that we prove to be secure in the sense of simulatability, which is the cryptographic notion of a secu re refinement. The correctness of this proof relies on a composition theorem and a deterministic bi simulation, which we formally verify using the theorem prover PVS. We further use PVS to formally v erify that message reordering is in fact prevented in the specification. We finally show that in tegrity properties are preserved under simulatability, which allows for carrying over the proven p ro erty to the concrete implementation. This yields the first example ever of a formally verified but ne vertheless cryptographically sound proof of a security protocol.

We present a general methodology for integrating arbitrary security requirements in the development of business processes in a b oth elegant and rigorous way. We show how trust relationships between differen t parties and their respective security goals can be reflected in a specification , which results in a realistic modeling of business processes in the presence of ma licious adversaries. Special attention is given to the incorporation of cryptogr aphy in the development process with the main goal of achieving specifications that a re sufficiently simple to be suited for formal verification, yet allow for a provably secure cryptographic implementation.