Search

Large language models (LLMs) can be used to analyze cyber threat intelligence (CTI) data from cybercrime forums, which contain extensive information and key discussions about emerging cyber threats. However, to date, the level of accuracy and efficiency of LLMs for such critical tasks has yet to be thoroughly evaluated. Hence, this study assesses the performance of an LLM system built on the OpenAI GPT-3.5-turbo model [8] to extract CTI information. To do so, a random sample of more than 700 daily conversations from three cybercrime forums - XSS, Exploit_in, and RAMP - was extracted, and the LLM system was instructed to summarize the conversations and predict 10 key CTI variables, such as whether a large organization and/or a critical infrastructure is being targeted, with only simple human-language instructions. Then, two coders reviewed each conversation and evaluated whether the information extracted by the LLM was accurate. The LLM system performed well, with an average accuracy score of 96.23%, an average precision of 90% and an average recall of 88.2%. Various ways to enhance the model were uncovered, such as the need to help the LLM distinguish between stories and past events, as well as being careful with verb tenses in prompts. Nevertheless, the results of this study highlight the relevance of using LLMs for cyber threat intelligence.

The intuitionistic modal logics considered between Constructive K (CK) and Intuitionistic K (IK) differ in their treatment of the possibility (diamond) connective. It was recently rediscovered that some logics between CK and IK also disagree on their diamond-free fragments, with only some remaining conservative over the standard axiomatisation of intuitionistic modal logic with necessity (box) alone. We show that relational Kripke semantics for CK can be extended with frame conditions for all axioms in the standard axiomatisation of IK, as well as other axioms previously studied. This allows us to answer open questions about the (non-)conservativity of such logics over intuitionistic modal logic without diamond. Our results are formalised using the Coq Proof Assistant.

[18F]-florbetaben positron emission tomography (PET) imaging is an established marker of {\ss}-Amyloid (A{\ss}) that is being increasingly used to assess A{\ss} deposition in AD. This study presents a novel, explainable machine learning-based biomarker for assessing A{\ss}+ positivity based on [18F]-florbetaben PET scans. We analyzed 163 scans acquired at our institution as part of a retrospective analysis. Initially, we used the regional loadings to train a Cubic Support Vector Machine (SVM) classifier and tested the model using 5-fold cross-validation. To elucidate the model's decision-making process in aggregate, we employed local interpretable model-agnostic explanations (LIME), projecting the most influential features back onto the AAL atlas for visualization. The Cubic SVM classifier demonstrated robust performance, achieving 92.0% accuracy and 90.5% precision under 5-fold cross-validation. LIME analysis revealed that the model identified critical regions impacting A{\ss}+ status, with notable contributions from the inferior frontal cortex, cuneus, olfactory cortex, postcentral gyrus, supramarginal gyrus, temporal pole, thalamus, and pallidum. The model showcases high accuracy, paralleling expert interpretation levels, and provides critical insights into the brain regions most affected by amyloid deposition. By elucidating the relationship between overall A{\ss}+ status and specific brain regions, our approach holds promise for novel insights into the correlation between the spatial distribution of A{\ss} and the clinical manifestations of AD., Comment: Submitted to the 2024 OHBM Annual Meeting

Decentralized finance (DeFi) has been the target of numerous profit-driven crimes, but the prevalence and cumulative impact of these crimes have not yet been assessed. This study provides a comprehensive assessment of profit-driven crimes targeting the DeFi sector. We collected data on 1141 crime events from 2017 to 2022. Of these, 1036 were related to DeFi (the main focus of this study) and 105 to centralized finance (CeFi). The findings show that the entire cryptoasset industry has suffered a minimum loss of US$30B, with two-thirds related to CeFi and one-third to DeFi. Focusing on DeFi, a taxonomy was developed to clarify the similarities and differences among these crimes. All events were mapped onto the DeFi stack to assess the impacted technical layers, and the financial damages were quantified to gauge their scale. The results highlight that during an attack, a DeFi actor (an entity developing a DeFi technology) can serve as a direct target (due to technical vulnerabilities or exploitation of human risks), as a perpetrator (through malicious uses of contracts or market manipulations), or as an intermediary (by being imitated through, for example, phishing scams). The findings also show that DeFi actors are the first victims of crimes targeting the DeFi industry: 52% of events targeted them, primarily due to technical vulnerabilities at the protocol layer, and these events accounted for 83% of all financial damages. Alternatively, in 41% of events, DeFi actors were themselves malicious perpetrators, predominantly misusing contracts at the cryptoasset layer (e.g. rug pull scams). However, these events accounted for only 17% of all financial damages. The study offers a preliminary assessment of the size and scope of crime events within the DeFi sector and highlights the vulnerable position of DeFi actors in the ecosystem.

Ransomware-as-a-service (RaaS) is increasing the scale and complexity of ransomware attacks. Understanding the internal operations behind RaaS has been a challenge due to the illegality of such activities. The recent chat leak of the Conti RaaS operator, one of the most infamous ransomware operators on the international scene, offers a key opportunity to better understand the inner workings of such organizations. This paper analyzes the main topic discussions in the Conti chat leak using machine learning techniques such as Natural Language Processing (NLP) and Latent Dirichlet Allocation (LDA), as well as visualization strategies. Five discussion topics are found: 1) Business, 2) Technical, 3) Internal tasking/Management, 4) Malware, and 5) Customer Service/Problem Solving. Moreover, the distribution of topics among Conti members shows that only 4% of individuals have specialized discussions while almost all individuals (96%) are all-rounders, meaning that their discussions revolve around the five topics. The results also indicate that a significant proportion of Conti discussions are non-tech related. This study thus highlights that running such large RaaS operations requires a workforce skilled beyond technical abilities, with individuals involved in various tasks, from management to customer service or problem solving. The discussion topics also show that the organization behind the Conti RaaS oper5086933ator shares similarities with a large firm. We conclude that, although RaaS represents an example of specialization in the cybercrime industry, only a few members are specialized in one topic, while the rest runs and coordinates the RaaS operation.

Compared to physical health, population mental health measurement in the U.S. is very coarse-grained. Currently, in the largest population surveys, such as those carried out by the Centers for Disease Control or Gallup, mental health is only broadly captured through "mentally unhealthy days" or "sadness", and limited to relatively infrequent state or metropolitan estimates. Through the large scale analysis of social media data, robust estimation of population mental health is feasible at much higher resolutions, up to weekly estimates for counties. In the present work, we validate a pipeline that uses a sample of 1.2 billion Tweets from 2 million geo-located users to estimate mental health changes for the two leading mental health conditions, depression and anxiety. We find moderate to large associations between the language-based mental health assessments and survey scores from Gallup for multiple levels of granularity, down to the county-week (fixed effects $\beta = .25$ to $1.58$; $p<.001$). Language-based assessment allows for the cost-effective and scalable monitoring of population mental health at weekly time scales. Such spatially fine-grained time series are well suited to monitor effects of societal events and policies as well as enable quasi-experimental study designs in population health and other disciplines. Beyond mental health in the U.S., this method generalizes to a broad set of psychological outcomes and allows for community measurement in under-resourced settings where no traditional survey measures - but social media data - are available., Comment: 9 pages, 7 figures, pre-print

Many activities related to cybercrime operations do not require much secrecy, such as developing websites or translating texts. This research provides indications that many users of a popular public internet marketing forum have connections to cybercrime. It does so by investigating the involvement in cybercrime of a population of users interested in internet marketing, both at a micro and macro scale. The research starts with a case study of three users confirmed to be involved in cybercrime and their use of the public forum where users share information about online advertising. It provides a first glimpse that some business with cybercrime connection is being conducted in the clear. The study then pans out to investigate the forum population's ties with cybercrime by finding crossover users, who are users from the public forum who also comment on cybercrime forums. The cybercrime forums on which they discuss are analyzed and crossover users' strength of participation is reported. Also, to assess if they represent a sub-group of the forum population, their posting behavior on the public forum is compared with that of non-crossover users. This blend of analyses shows that (i) a minimum of 7.2% of the public forum population are crossover users that have ties with cybercrime forums; (ii) their participation in cybercrime forums is limited; and (iii) their posting behavior is relatively indistinguishable from that of non-crossover users. This is the first study to formally quantify how users of an internet marketing public forum, a space for informal exchanges, have ties to cybercrime activities. We conclude that crossover users are a substantial part of the population in the public forum, and, even though they have thus far been overlooked, their aggregated effect in the ecosystem must be considered., Comment: 18 pages, 4 figures

Background: Oral histories from 9/11 responders to the World Trade Center (WTC) attacks provide rich narratives about distress and resilience. Artificial Intelligence (AI) models promise to detect psychopathology in natural language, but they have been evaluated primarily in non-clinical settings using social media. This study sought to test the ability of AI-based language assessments to predict PTSD symptom trajectories among responders. Methods: Participants were 124 responders whose health was monitored at the Stony Brook WTC Health and Wellness Program who completed oral history interviews about their initial WTC experiences. PTSD symptom severity was measured longitudinally using the PTSD Checklist (PCL) for up to 7 years post-interview. AI-based indicators were computed for depression, anxiety, neuroticism, and extraversion along with dictionary-based measures of linguistic and interpersonal style. Linear regression and multilevel models estimated associations of AI indicators with concurrent and subsequent PTSD symptom severity (significance adjusted by false discovery rate). Results: Cross-sectionally, greater depressive language (beta=0.32; p=0.043) and first-person singular usage (beta=0.31; p=0.044) were associated with increased symptom severity. Longitudinally, anxious language predicted future worsening in PCL scores (beta=0.31; p=0.031), whereas first-person plural usage (beta=-0.37; p=0.007) and longer words usage (beta=-0.36; p=0.007) predicted improvement. Conclusions: This is the first study to demonstrate the value of AI in understanding PTSD in a vulnerable population. Future studies should extend this application to other trauma exposures and to other demographic groups, especially under-represented minorities., Comment: 20 pages, 2 figures

We provide a direct method for proving Craig interpolation for a range of modal and intuitionistic logics, including those containing a "converse" modality. We demonstrate this method for classical tense logic, its extensions with path axioms, and for bi-intuitionistic logic. These logics do not have straightforward formalisations in the traditional Gentzen-style sequent calculus, but have all been shown to have cut-free nested sequent calculi. The proof of the interpolation theorem uses these calculi and is purely syntactic, without resorting to embeddings, semantic arguments, or interpreted connectives external to the underlying logical language. A novel feature of our proof includes an orthogonality condition for defining duality between interpolants., Comment: Appended version of the paper "Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic via Nested Sequents", accepted to the 28th International Conference on Computer Science Logic (CSL 2020)

In the past year, a new spamming scheme has emerged: sexual extortion messages requiring payments in the cryptocurrency Bitcoin, also known as sextortion. This scheme represents a first integration of the use of cryptocurrencies by members of the spamming industry. Using a dataset of 4,340,736 sextortion spams, this research aims at understanding such new amalgamation by uncovering spammers' operations. To do so, a simple, yet effective method for projecting Bitcoin addresses mentioned in sextortion spams onto transaction graph abstractions is computed over the entire Bitcoin blockchain. This allows us to track and investigate monetary flows between involved actors and gain insights into the financial structure of sextortion campaigns. We find that sextortion spammers are somewhat sophisticated, following pricing strategies and benefiting from cost reductions as their operations cut the upper-tail of the spamming supply chain. We discover that one single entity is likely controlling the financial backbone of the majority of the sextortion campaigns and that the 11-month operation studied yielded a lower-bound revenue between \$1,300,620 and \$1,352,266. We conclude that sextortion spamming is a lucrative business and spammers will likely continue to send bulk emails that try to extort money through cryptocurrencies., Comment: 12 pages, 5 figures, Advances in Financial Technologies (AFT 2019)

In recent years we have seen several new models of dependent type theory extended with some form of modal necessity operator, including nominal type theory, guarded and clocked type theory, and spatial and cohesive type theory. In this paper we study modal dependent type theory: dependent type theory with an operator satisfying (a dependent version of) the K-axiom of modal logic. We investigate both semantics and syntax. For the semantics, we introduce categories with families with a dependent right adjoint (CwDRA) and show that the examples above can be presented as such. Indeed, we show that any finite limit category with an adjunction of endofunctors gives rise to a CwDRA via the local universe construction. For the syntax, we introduce a dependently typed extension of Fitch-style modal lambda-calculus, show that it can be interpreted in any CwDRA, and build a term model. We extend the syntax and semantics with universes.

Ransomware can prevent a user from accessing a device and its files until a ransom is paid to the attacker, most frequently in Bitcoin. With over 500 known ransomware families, it has become one of the dominant cybercrime threats for law enforcement, security professionals and the public. However, a more comprehensive, evidence-based picture on the global direct financial impact of ransomware attacks is still missing. In this paper, we present a data-driven method for identifying and gathering information on Bitcoin transactions related to illicit activity based on footprints left on the public Bitcoin blockchain. We implement this method on-top-of the GraphSense open-source platform and apply it to empirically analyze transactions related to 35 ransomware families. We estimate the lower bound direct financial impact of each ransomware family and find that, from 2013 to mid-2017, the market for ransomware payments has a minimum worth of USD 12,768,536 (22,967.54 BTC). We also find that the market is highly skewed with only a few number of players responsible for the majority of the payments. Based on these research findings, policy-makers and law enforcement agencies can use the statistics provided to understand the size of the illicit market and make informed decisions on how best to address the threat., Comment: 17th Annual Workshop on the Economics of Information Security (WEIS)

Abstract separation logics are a family of extensions of Hoare logic for reasoning about programs that manipulate resources such as memory locations. These logics are "abstract" because they are independent of any particular concrete resource model. Their assertion languages, called propositional abstract separation logics (PASLs), extend the logic of (Boolean) Bunched Implications (BBI) in various ways. In particular, these logics contain the connectives $*$ and $-\!*$, denoting the composition and extension of resources respectively. This added expressive power comes at a price since the resulting logics are all undecidable. Given their wide applicability, even a semi-decision procedure for these logics is desirable. Although several PASLs and their relationships with BBI are discussed in the literature, the proof theory and automated reasoning for these logics were open problems solved by the conference version of this paper, which developed a modular proof theory for various PASLs using cut-free labelled sequent calculi. This paper non-trivially improves upon this previous work by giving a general framework of calculi on which any new axiom in the logic satisfying a certain form corresponds to an inference rule in our framework, and the completeness proof is generalised to consider such axioms. Our base calculus handles Calcagno et al.'s original logic of separation algebras by adding sound rules for partial-determinism and cancellativity, while preserving cut-elimination. We then show that many important properties in separation logic, such as indivisible unit, disjointness, splittability, and cross-split, can be expressed in our general axiom form. Thus our framework offers inference rules and completeness for these properties for free. Finally, we show how our calculi reduce to calculi with global label substitutions, enabling more efficient implementation., Comment: Accepted for publication in ACM Transactions on Computational Logic (TOCL). arXiv admin note: text overlap with arXiv:1307.5592

Fitch-style modal deduction, in which modalities are eliminated by opening a subordinate proof, and introduced by shutting one, were investigated in the 1990s as a basis for lambda calculi. We show that such calculi have good computational properties for a variety of intuitionistic modal logics. Semantics are given in cartesian closed categories equipped with an adjunction of endofunctors, with the necessity modality interpreted by the right adjoint. Where this functor is an idempotent comonad, a coherence result on the semantics allows us to present a calculus for intuitionistic S4 that is simpler than others in the literature. We show the calculi can be extended \`{a} la tense logic with the left adjoint of necessity, and are then complete for the categorical semantics., Comment: Accepted paper at the 21st International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2018). This version includes appendices containing many proof details

This paper improves the treatment of equality in guarded dependent type theory (GDTT), by combining it with cubical type theory (CTT). GDTT is an extensional type theory with guarded recursive types, which are useful for building models of program logics, and for programming and reasoning with coinductive types. We wish to implement GDTT with decidable type checking, while still supporting non-trivial equality proofs that reason about the extensions of guarded recursive constructions. CTT is a variation of Martin-L\"of type theory in which the identity type is replaced by abstract paths between terms. CTT provides a computational interpretation of functional extensionality, enjoys canonicity for the natural numbers type, and is conjectured to support decidable type-checking. Our new type theory, guarded cubical type theory (GCTT), provides a computational interpretation of extensionality for guarded recursive types. This further expands the foundations of CTT as a basis for formalisation in mathematics and computer science. We present examples to demonstrate the expressivity of our type theory, all of which have been checked using a prototype type-checker implementation. We show that CTT can be given semantics in presheaves on the product of the cube category and a small category with an initial object. We then show that the category of presheaves on the product of the cube category and omega provides semantics for GCTT., Comment: Final version; Special Issue on Homotopy Type Theory and Univalent Foundations, Journal of Automated Reasoning, 2017

We present the guarded lambda-calculus, an extension of the simply typed lambda-calculus with guarded recursive and coinductive types. The use of guarded recursive types ensures the productivity of well-typed programs. Guarded recursive types may be transformed into coinductive types by a type-former inspired by modal logic and Atkey-McBride clock quantification, allowing the typing of acausal functions. We give a call-by-name operational semantics for the calculus, and define adequate denotational semantics in the topos of trees. The adequacy proof entails that the evaluation of a program always terminates. We introduce a program logic with L\"ob induction for reasoning about the contextual equivalence of programs. We demonstrate the expressiveness of the calculus by showing the definability of solutions to Rutten's behavioural differential equations., Comment: Accepted to Logical Methods in Computer Science special issue on the 18th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2015)

This paper improves the treatment of equality in guarded dependent type theory (GDTT), by combining it with cubical type theory (CTT). GDTT is an extensional type theory with guarded recursive types, which are useful for building models of program logics, and for programming and reasoning with coinductive types. We wish to implement GDTT with decidable type-checking, while still supporting non-trivial equality proofs that reason about the extensions of guarded recursive constructions. CTT is a variation of Martin-L\"of type theory in which the identity type is replaced by abstract paths between terms. CTT provides a computational interpretation of functional extensionality, is conjectured to have decidable type checking, and has an implemented type-checker. Our new type theory, called guarded cubical type theory, provides a computational interpretation of extensionality for guarded recursive types. This further expands the foundations of CTT as a basis for formalisation in mathematics and computer science. We present examples to demonstrate the expressivity of our type theory, all of which have been checked using a prototype type-checker implementation, and present semantics in a presheaf category., Comment: 17 pages, to be published in proceedings of CSL 2016

We present guarded dependent type theory, gDTT, an extensional dependent type theory with a `later' modality and clock quantifiers for programming and proving with guarded recursive and coinductive types. The later modality is used to ensure the productivity of recursive definitions in a modular, type based, way. Clock quantifiers are used for controlled elimination of the later modality and for encoding coinductive types using guarded recursive types. Key to the development of gDTT are novel type and term formers involving what we call `delayed substitutions'. These generalise the applicative functor rules for the later modality considered in earlier work, and are crucial for programming and proving with dependent types. We show soundness of the type theory with respect to a denotational model., Comment: This is the technical report version of a paper to appear in the proceedings of FoSSaCS 2016

Nakano's "later" modality, inspired by G\"{o}del-L\"{o}b provability logic, has been applied in type systems and program logics to capture guarded recursion. Birkedal et al modelled this modality via the internal logic of the topos of trees. We show that the semantics of the propositional fragment of this logic can be given by linear converse-well-founded intuitionistic Kripke frames, so this logic is a marriage of the intuitionistic modal logic KM and the intermediate logic LC. We therefore call this logic $\mathrm{KM}_{\mathrm{lin}}$. We give a sound and cut-free complete sequent calculus for $\mathrm{KM}_{\mathrm{lin}}$ via a strategy that decomposes implication into its static and irreflexive components. Our calculus provides deterministic and terminating backward proof-search, yields decidability of the logic and the coNP-completeness of its validity problem. Our calculus and decision procedure can be restricted to drop linearity and hence capture KM., Comment: Extended version, with full proof details, of a paper accepted to FoSSaCS 2015 (this version edited to fix some minor typos)

We present the guarded lambda-calculus, an extension of the simply typed lambda-calculus with guarded recursive and coinductive types. The use of guarded recursive types ensures the productivity of well-typed programs. Guarded recursive types may be transformed into coinductive types by a type-former inspired by modal logic and Atkey-McBride clock quantification, allowing the typing of acausal functions. We give a call-by-name operational semantics for the calculus, and define adequate denotational semantics in the topos of trees. The adequacy proof entails that the evaluation of a program always terminates. We demonstrate the expressiveness of the calculus by showing the definability of solutions to Rutten's behavioural differential equations. We introduce a program logic with L\"{o}b induction for reasoning about the contextual equivalence of programs., Comment: Version of FoSSaCS 2015 paper with appendices

Separation logics are a family of extensions of Hoare logic for reasoning about programs that mutate memory. These logics are "abstract" because they are independent of any particular concrete memory model. Their assertion languages, called propositional abstract separation logics, extend the logic of (Boolean) Bunched Implications (BBI) in various ways. We develop a modular proof theory for various propositional abstract separation logics using cut-free labelled sequent calculi. We first extend the cut-fee labelled sequent calculus for BBI of Hou et al to handle Calcagno et al's original logic of separation algebras by adding sound rules for partial-determinism and cancellativity, while preserving cut-elimination. We prove the completeness of our calculus via a sound intermediate calculus that enables us to construct counter-models from the failure to find a proof. We then capture other propositional abstract separation logics by adding sound rules for indivisible unit and disjointness, while maintaining completeness. We present a theorem prover based on our labelled calculus for these propositional abstract separation logics.

Full Intuitionistic Linear Logic (FILL) is multiplicative intuitionistic linear logic extended with par. Its proof theory has been notoriously difficult to get right, and existing sequent calculi all involve inference rules with complex annotations to guarantee soundness and cut-elimination. We give a simple and annotation-free display calculus for FILL which satisfies Belnap's generic cut-elimination theorem. To do so, our display calculus actually handles an extension of FILL, called Bi-Intuitionistic Linear Logic (BiILL), with an `exclusion' connective defined via an adjunction with par. We refine our display calculus for BiILL into a cut-free nested sequent calculus with deep inference in which the explicit structural rules of the display calculus become admissible. A separation property guarantees that proofs of FILL formulae in the deep inference calculus contain no trace of exclusion. Each such rule is sound for the semantics of FILL, thus our deep inference calculus and display calculus are conservative over FILL. The deep inference calculus also enjoys the subformula property and terminating backward proof search, which gives the NP-completeness of BiILL and FILL.

Many formal systems, particularly in computer science, may be captured by equations modulated by side conditions asserting the "freshness of names"; these can be reasoned about with Nominal Equational Logic (NEL). Like most logics of this sort NEL employs this notion of freshness as a first class logical connective. However, this can become inconvenient when attempting to translate results from standard equational logic to the nominal setting. This paper presents proof rules for a logic whose only connectives are equations, which we call Nominal Equation-only Logic (NEoL). We prove that NEoL is just as expressive as NEL. We then give a simple description of equality in the empty NEoL-theory, then extend that result to describe freshness in the empty NEL-theory., Comment: In Proceedings LFMTP 2011, arXiv:1110.6685