K. Rustan M. Leino

131 papers A* 6A 16B 23C 2Misc 2Journal 30Unranked 48
YearRankTypeTitle / Venue / Authors
2026 conf
On the Pursuit of Insight and Elegance
K. Rustan M. Leino
2025 A* conf
ICSE
Aleks Chakarov, Jaco Geldenhuys, Matthew Heck, Michael Hicks, Sam Huang, Georges-Axel Jaloyan, Anjali Joshi, K. Rustan M. Leino, Mikael Mayer, Sean McLaughlin, Akhilesh Mritunjai, Clément Pit-Claudel, Sorawee Porncharoenwase, Florian Rabe, Marianna Rapoport, Giles Reger, Cody Roux, Neha Rungta, Robin Salkeld, Matthias Schlaipfer, Daniel Schoepe, Johanna Schwartzentruber, Serdar Tasiran, Aaron Tomb, Emina Torlak, Jean-Baptiste Tristan, Lucas G. Wagner, Michael W. Whalen, Remy Willems, Tongtong Xiang, Tae Joon Byun, Joshua M. Cohen, Ruijie Fang, Junyoung Jang, Jakob Rath, Hira Taqdees Syeda, Dominik Wagner, Yongwei Yuan
2025 J jnl
CoRR
Stefan Ciobâca, K. Rustan M. Leino, Stefan-Alexandru Mercas, Roxana-Mihaela Timon
2024 conf
FM (1)
Tabea Bordis, K. Rustan M. Leino
2024 J jnl
Formal Methods Syst. Des.
Aws Albarghouthi, K. Rustan M. Leino, Alexandra Silva, Caterina Urban
2024 B conf
FMCAD
K. Rustan M. Leino
2022 conf
The Logic of Software. A Tasting Menu of Formal Methods
David R. Cok, K. Rustan M. Leino
2021 ed.
CAV (1)
Alexandra Silva, K. Rustan M. Leino
2021 ed.
CAV (2)
Alexandra Silva, K. Rustan M. Leino
2018 conf
Principled Software Development
K. Rustan M. Leino, Daniel Matichuk
2017 J jnl
IEEE Softw.
K. Rustan M. Leino
2017 conf
SNAPL
Karthikeyan Bhargavan, Barry Bond, Antoine Delignat-Lavaud, Cédric Fournet, Chris Hawblitzel, Catalin Hritcu, Samin Ishtiaq, Markulf Kohlweiss, K. Rustan M. Leino, Jay R. Lorch, Kenji Maillard, Jianyang Pan, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella-Béguelin, Jean Karim Zinzindohoue
2017 conf
SETSS
K. Rustan M. Leino
2017 A* conf
USENIX Security Symposium
Barry Bond, Chris Hawblitzel, Manos Kapritsos, K. Rustan M. Leino, Jacob R. Lorch, Bryan Parno, Ashay Rane, Srinath T. V. Setty, Laure Thompson
2016 A conf
TACAS
Maria Christakis, K. Rustan M. Leino, Peter Müller, Valentin Wüstholz
2016 conf
Theory and Practice of Formal Methods
Razvan Certezeanu, Sophia Drossopoulou, Benjamin Egelund-Müller, K. Rustan M. Leino, Sinduran Sivarajan, Mark J. Wheelhouse
2016 conf
CAV (1)
K. Rustan M. Leino, Clément Pit-Claudel
2016 B ed.
VMCAI
Barbara Jobstmann, K. Rustan M. Leino
2015 J jnl
ACM Trans. Comput. Log.
K. Rustan M. Leino, Paqui Lucio
2015 conf
FTfJP@ECOOP
Reza Ahmadi, K. Rustan M. Leino, Jyrki Nummenmaa
2015 conf
LPAR (short papers)
K. Rustan M. Leino
2015 conf
CAV (1)
K. Rustan M. Leino, Valentin Wüstholz
2015 conf
Refine@FM
Jason Koenig, K. Rustan M. Leino
2015 conf
IWIL@LPAR
K. Rustan M. Leino
2014 B conf
FM
K. Rustan M. Leino, Michal Moskal
2014 conf
TAP@STAF
Nada Amin, K. Rustan M. Leino, Tiark Rompf
2014 B conf
FM
Maria Christakis, K. Rustan M. Leino, Wolfram Schulte
2014 conf
F-IDE
K. Rustan M. Leino, Valentin Wüstholz
2013 B conf
VMCAI
Stefan Heule, K. Rustan M. Leino, Peter Müller, Alexander J. Summers
2013 B conf
ITP
K. Rustan M. Leino
2013 A* conf
ICSE
K. Rustan M. Leino
2013 J jnl
ACM SIGPLAN Notices
Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, Raymie Stata
2013 J jnl
Int. J. Softw. Tools Technol. Transf.
Parosh Aziz Abdulla, K. Rustan M. Leino
2013 conf
VSTTE
K. Rustan M. Leino, Nadia Polikarpova
2012 B conf
VMCAI
K. Rustan M. Leino
2012 J jnl
ACM Comput. Surv.
John Hatcliff, Gary T. Leavens, K. Rustan M. Leino, Peter Müller, Matthew J. Parkinson
2012 conf
VSTTE
K. Rustan M. Leino
2012 conf
HILT
K. Rustan M. Leino
2012 ch.
Software Safety and Security
Jason Koenig, K. Rustan M. Leino
2012 A conf
OOPSLA
K. Rustan M. Leino, Aleksandar Milicevic
2012 conf
HILT
K. Rustan M. Leino
2012 conf
SPLASH
K. Rustan M. Leino
2012 J jnl
Formal Aspects Comput.
K. Rustan M. Leino, Kuat Yessenov
2012 conf
TOPI@ICSE
Néstor Cataño, K. Rustan M. Leino, Víctor Rivera
2011 conf
FTfJP@ECOOP
Stefan Heule, K. Rustan M. Leino, Peter Müller, Alexander J. Summers
2011 conf
NASA Formal Methods
K. Rustan M. Leino
2011 J jnl
Commun. ACM
Mike Barnett, Manuel Fähndrich, K. Rustan M. Leino, Peter Müller, Wolfram Schulte, Herman Venter
2011 B conf
FM
Vladimir Klebanov, Peter Müller, Natarajan Shankar, Gary T. Leavens, Valentin Wüstholz, Eyad Alkassar, Rob Arthan, Derek Bronish, Rod Chapman, Ernie Cohen, Mark A. Hillebrand, Bart Jacobs, K. Rustan M. Leino, Rosemary Monahan, Frank Piessens, Nadia Polikarpova, Tom Ridge, Jan Smans, Stephan Tobies, Thomas Tuerk, Mattias Ulbrich, Benjamin Weiß
2011 B conf
SEFM
Claire Le Goues, K. Rustan M. Leino, Michal Moskal
2011 A ed.
TACAS
Parosh Aziz Abdulla, K. Rustan M. Leino
2011 conf
LASER Summer School
Luke Herbert, K. Rustan M. Leino, Jose Quaresma
2010 A conf
TACAS
K. Rustan M. Leino, Philipp Rümmer
2010 conf
VSTTE
K. Rustan M. Leino, Rosemary Monahan
2010 conf
LPAR (Dakar)
K. Rustan M. Leino
2010 A conf
ESOP
K. Rustan M. Leino, Peter Müller, Jan Smans
2010 J jnl
Formal Methods Syst. Des.
Jochen Hoenicke, K. Rustan M. Leino, Andreas Podelski, Martin Schäf, Thomas Wies
2010 J jnl
Commun. ACM
K. Rustan M. Leino
2010 conf
VSTTE
Michael Barnett, K. Rustan M. Leino
2010 conf
The Future of Software Engineering
K. Rustan M. Leino
2010 B conf
VMCAI
K. Rustan M. Leino
2009 A conf
ESOP
K. Rustan M. Leino, Peter Müller
2009 B conf
FM
Jochen Hoenicke, K. Rustan M. Leino, Andreas Podelski, Martin Schäf, Thomas Wies
2009 B conf
FASE
K. Rustan M. Leino, Ronald Middelkoop
2009 Misc conf
SAC
K. Rustan M. Leino, Rosemary Monahan
2009 conf
FOSAD
K. Rustan M. Leino, Peter Müller, Jan Smans
2008 J jnl
ACM Trans. Program. Lang. Syst.
Bart Jacobs, Frank Piessens, Jan Smans, K. Rustan M. Leino, Wolfram Schulte
2008 conf
ISEC
K. Rustan M. Leino, Angela Wallenburg
2008 conf
VSTTE
K. Rustan M. Leino, Peter Müller, Angela Wallenburg
2008 conf
TPHOLs
Sascha Böhme, K. Rustan M. Leino, Burkhart Wolff
2008 B conf
COMPSAC
K. Rustan M. Leino
2008 conf
LASER Summer School
K. Rustan M. Leino, Peter Müller
2008 A conf
ESOP
K. Rustan M. Leino, Peter Müller
2007 A conf
CADE
K. Rustan M. Leino
2007 B conf
FASE
Ádám Darvas, K. Rustan M. Leino
2007 J jnl
Formal Aspects Comput.
Gary T. Leavens, K. Rustan M. Leino, Peter Müller
2007 A* conf
ASE
K. Rustan M. Leino
2007 A conf
ESOP
K. Rustan M. Leino, Wolfram Schulte
2007 A conf
TACAS
K. Rustan M. Leino
2006 A conf
ESOP
K. Rustan M. Leino, Peter Müller
2006 conf
Ershov Memorial Conference
K. Rustan M. Leino
2005 A conf
TACAS
K. Rustan M. Leino, Madan Musuvathi, Xinming Ou
2005 B conf
VMCAI
Bor-Yuh Evan Chang, K. Rustan M. Leino
2005 J jnl
Int. J. Softw. Tools Technol. Transf.
Lilian Burdy, Yoonsik Cheon, David R. Cok, Michael D. Ernst, Joseph R. Kiniry, Gary T. Leavens, K. Rustan M. Leino, Erik Poll
2005 conf
FMCO
Michael Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, K. Rustan M. Leino
2005 J jnl
Inf. Process. Lett.
K. Rustan M. Leino
2005 J jnl
Sci. Comput. Program.
K. Rustan M. Leino, Todd D. Millstein, James B. Saxe
2005 conf
AIOOL@VMCAI
Bor-Yuh Evan Chang, K. Rustan M. Leino
2005 B conf
SEFM
K. Rustan M. Leino
2005 B conf
APLAS
K. Rustan M. Leino, Francesco Logozzo
2005 B conf
FM
K. Rustan M. Leino, Peter Müller
2005 conf
Abstract State Machines
K. Rustan M. Leino
2005 B conf
SEFM
Bart Jacobs, Frank Piessens, K. Rustan M. Leino, Wolfram Schulte
2005 conf
VSTTE
Michael Barnett, Robert DeLine, Manuel Fähndrich, Bart Jacobs, K. Rustan M. Leino, Wolfram Schulte, Herman Venter
2005 conf
PASTE
Michael Barnett, K. Rustan M. Leino
2004 C conf
ICTAC
K. Rustan M. Leino
2004 B conf
SEFM
K. Rustan M. Leino, Wolfram Schulte
2004 J jnl
Concurr. Pract. Exp.
Michael Burrows, K. Rustan M. Leino
2004 A conf
ECOOP
K. Rustan M. Leino, Peter Müller
2004 J jnl
CoRR
Viktor Kuncak, K. Rustan M. Leino
2004 conf
CASSIS
Mike Barnett, K. Rustan M. Leino, Wolfram Schulte
2004 J jnl
J. Object Technol.
Michael Barnett, Robert DeLine, Manuel Fähndrich, K. Rustan M. Leino, Wolfram Schulte
2003 conf
Verification: Theory and Practice
Martín Abadi, K. Rustan M. Leino
2003 conf
SPIN
K. Rustan M. Leino
2003 C conf
FMICS
Lilian Burdy, Yoonsik Cheon, David R. Cok, Michael D. Ernst, Joseph Kiniry, Gary T. Leavens, K. Rustan M. Leino, Erik Poll
2003 A conf
OOPSLA
Manuel Fähndrich, K. Rustan M. Leino
2002 J jnl
ACM Trans. Program. Lang. Syst.
K. Rustan M. Leino, Greg Nelson
2002 A* conf
PLDI
Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, Raymie Stata
2002 A* conf
PLDI
K. Rustan M. Leino, Arnd Poetzsch-Heffter, Yunhong Zhou
2001 J jnl
Inf. Process. Lett.
Cormac Flanagan, Rajeev Joshi, K. Rustan M. Leino
2001 B conf
SAS
K. Rustan M. Leino
2001 Misc conf
Informatics
K. Rustan M. Leino
2001 conf
FME
Cormac Flanagan, K. Rustan M. Leino
2001 J jnl
Inf. Process. Lett.
K. Rustan M. Leino
2000 J jnl
Sci. Comput. Program.
Rajeev Joshi, K. Rustan M. Leino
2000 conf
OOPSLA Addendum
Gary T. Leavens, Clyde Ruby, K. Rustan M. Leino, Erik Poll, Bart Jacobs
1999 conf
ECOOP Workshops
K. Rustan M. Leino, James B. Saxe, Raymie Stata
1999 J jnl
Formal Aspects Comput.
K. Rustan M. Leino
1999 J jnl
Theor. Comput. Sci.
K. Rustan M. Leino, Rajit Manohar
1999 J jnl
Inf. Process. Lett.
K. Rustan M. Leino, Raymie Stata
1998 B conf
MPC
K. Rustan M. Leino, Rajeev Joshi
1998 B conf
CC
K. Rustan M. Leino, Greg Nelson
1998 A conf
OOPSLA
K. Rustan M. Leino
1998 conf
PROCOMET
K. Rustan M. Leino
1998 A conf
ESOP
K. Rustan M. Leino
1998 J jnl
Nord. J. Comput.
K. Rustan M. Leino
1997 conf
TAPSOFT
Martín Abadi, K. Rustan M. Leino
1995 J jnl
Formal Aspects Comput.
K. Rustan M. Leino
1995 J jnl
Formal Aspects Comput.
Rajit Manohar, K. Rustan M. Leino
1995 J jnl
Inf. Process. Lett.
K. Rustan M. Leino
1995
K. Rustan M. Leino
1994 conf
PROCOMET
K. Rustan M. Leino, Jan L. A. van de Snepscheut
redb/extractors/macho_extractors/macho_universal.py
← Index redb/extractors/macho_extractors/macho_universal.py python
import hashlib
import inspect
import json
from datetime import datetime, timezone
from typing import Any, List

from redb.extractors.enum import Tag
from redb.extractors.macho_extractor import MachOExtractor
from redb.models.dataclasses import MachOUniversal


class MachOUniversalExtractor(MachOExtractor):

    def __init__(
        self,
        filepath,
        log,
        exporters=None,
        index_prefix=None,
        elastic_index=None,
        known_benign=False,
        known_malicious=False,
        macho=None,
    ):
        super().__init__(
            filepath,
            log,
            exporters,
            index_prefix,
            elastic_index,
            known_benign,
            known_malicious,
            macho,
        )
        self.elastic_index = self.index_prefix + "-macho_universal"
        self.log.debug(inspect.currentframe().f_code.co_name)

    def tag(self):
        return Tag.MACHO_UNIVERSAL.value

    def _extract_universal_info(self):
        """Extract Universal/FAT binary architecture information using new API."""
        self.log.debug(inspect.currentframe().f_code.co_name)

        if not self.macho:
            return None

        try:
            # Parse at Universal level first (new API requirement)
            self.macho.parse()

            # Get architectures using new API
            architectures = self.macho.get_architectures()
            if not architectures:
                return None

            # Check if this is a FAT binary
            is_fat = len(architectures) > 1

            architecture_info = []

            # Extract info for each architecture
            for arch_name in architectures:
                try:
                    # Get general info for this architecture
                    general_info = self.macho.get_general_info(arch=arch_name)

                    # Get header info for this architecture
                    header_info = self.macho.get_macho_header(arch=arch_name)

                    # Get architecture-specific MachO instance for detailed analysis
                    arch_macho = self.macho.get_macho_for_arch(arch_name)

                    # Calculate architecture slice hash (if we can access the raw data)
                    arch_sha256 = None
                    arch_md5 = None
                    arch_sha1 = None

                    # For FAT binaries, try to get slice-specific info
                    if is_fat and arch_macho:
                        try:
                            # This would require access to the slice data
                            # For now, we'll use the general file info
                            arch_sha256 = general_info.get('SHA256', '') if general_info else ''
                            arch_md5 = general_info.get('MD5', '') if general_info else ''
                            arch_sha1 = general_info.get('SHA1', '') if general_info else ''
                        except Exception as e:
                            self.log.debug(f"Could not extract slice hash for {arch_name}: {e}")

                    architecture_info.append({
                        'architecture': arch_name,
                        'arch_sha256': arch_sha256,
                        'arch_md5': arch_md5,
                        'arch_sha1': arch_sha1,
                        'cputype': header_info.get('cputype') if header_info else None,
                        'cpusubtype': header_info.get('cpusubtype') if header_info else None,
                        'filetype': header_info.get('filetype') if header_info else None
                    })

                except Exception as e:
                    self.log.warning(f"Error extracting info for architecture {arch_name}: {e}")
                    continue

            # Create Universal dataclass
            macho_universal = MachOUniversal(
                is_fat=is_fat,
                architecture_count=len(architectures),
                architectures=architectures,
                architecture_info=architecture_info,
                fat_hash=self.sha256,
                fat_md5=self.md5,
                fat_sha1=self.sha1
            )

            return macho_universal

        except Exception as e:
            self.log.error(f"Error extracting MachO Universal info: {e}")
            return None

    def _extract_fat_architecture_mappings(self):
        """Extract detailed FAT binary architecture mappings for database relationships."""
        self.log.debug(inspect.currentframe().f_code.co_name)

        if not self.macho:
            return []

        try:
            # Parse at Universal level first
            self.macho.parse()

            # Get architectures using new API
            architectures = self.macho.get_architectures()
            if not architectures or len(architectures) <= 1:
                return []  # Not a FAT binary

            mappings = []
            current_time = datetime.now(timezone.utc)

            # For each architecture, create a mapping record
            for arch_name in architectures:
                try:
                    # Get general info
                    general_info = self.macho.get_general_info()

                    # Create mapping record for FAT binary architecture table
                    mapping = {
                        'fat_hash': self.sha256,  # SHA256 of the FAT binary
                        'architecture': arch_name,
                        'arch_sha256': general_info.get('SHA256', '') if general_info else '',  # Will need proper slice extraction
                        'arch_md5': general_info.get('MD5', '') if general_info else '',
                        'arch_sha1': general_info.get('SHA1', '') if general_info else '',
                        'arch_filename': f"{general_info.get('Filename', '')}.{arch_name}" if general_info else '',
                        'analysis_date': current_time
                    }
                    mappings.append(mapping)

                except Exception as e:
                    self.log.warning(f"Error creating mapping for architecture {arch_name}: {e}")
                    continue

            return mappings

        except Exception as e:
            self.log.error(f"Error extracting FAT architecture mappings: {e}")
            return []

    def extract(self):
        self.log.debug(inspect.currentframe().f_code.co_name)
        try:
            universal_info = self._extract_universal_info()
            return universal_info
        except Exception as e:
            self.log.error(f"Error extracting MachO Universal info: {e}")
            return None

    def extract_fat_binary_basic_properties_data(self):
        """Extract data needed for creating multiple BasicProperties records for FAT binaries.

        Returns:
            Tuple: (is_fat, fat_sha256, architectures_info) where:
                - is_fat: bool indicating if this is a FAT binary
                - fat_sha256: SHA256 of the FAT wrapper
                - architectures_info: dict with arch names and their hashes
        """
        self.log.debug(inspect.currentframe().f_code.co_name)

        if not self.macho:
            return False, None, {}

        try:
            # Parse at Universal level first
            self.macho.parse()

            # Get architectures using new API
            architectures = self.macho.get_architectures()
            if not architectures or len(architectures) <= 1:
                return False, None, {}  # Not a FAT binary

            # This is a FAT binary
            architectures_info = {}

            for arch_name in architectures:
                try:
                    # Get general info for this architecture
                    general_info = self.macho.get_general_info(arch=arch_name)

                    if general_info:
                        architectures_info[arch_name] = {
                            'sha256': general_info.get('SHA256', ''),
                            'md5': general_info.get('MD5', ''),
                            'sha1': general_info.get('SHA1', ''),
                            'filename': general_info.get('Filename', ''),
                            'filesize': general_info.get('Filesize', 0)
                        }
                except Exception as e:
                    self.log.warning(f"Error extracting info for architecture {arch_name}: {e}")
                    continue

            return True, self.sha256, architectures_info

        except Exception as e:
            self.log.error(f"Error extracting FAT binary data: {e}")
            return False, None, {}

    def prepare_export_data(self, exporter_type: str) -> Any:
        if exporter_type == "ElasticsearchExporter":
            return self.extract()
        elif exporter_type == "ClickHouseExporter":
            universal_info = self.extract()
            if universal_info is None:
                return None

            data = []
            current_time = datetime.now(timezone.utc)

            # Get architecture info for the binary
            try:
                if universal_info.is_fat:
                    # For FAT binaries, architecture fields should be NULL since it contains multiple
                    architecture_raw = None
                    architecture_str = None
                else:
                    # For single-arch binaries, get the actual architecture info
                    header_info = self.macho.get_macho_header()
                    architecture_raw = header_info.get('cputype', 0) if header_info else 0
                    architecture_str = universal_info.architectures[0] if universal_info.architectures else None
            except Exception as e:
                self.log.warning(f"Could not get architecture info for binary: {e}")
                architecture_raw = None
                architecture_str = None

            # Main Universal binary record
            data.append([
                self.sha256,                              # sha256
                self.md5,                                 # md5
                self.sha1,                                # sha1
                None,                                     # parent_sha256 (always None for main FAT binary)
                architecture_raw,                         # architecture (raw CPU type)
                architecture_str,                         # architecture_str (human-readable)
                universal_info.is_fat,                    # is_fat
                universal_info.architecture_count,       # architecture_count
                universal_info.architectures,            # architectures (array)
                json.dumps(universal_info.architecture_info[0] if len(universal_info.architecture_info) == 1 else {"architectures": universal_info.architecture_info}) if universal_info.architecture_info else None,  # architecture_info (JSON)
                current_time,                             # analysis_date
            ])

            column_names = [
                'sha256', 'md5', 'sha1', 'parent_sha256', 'architecture', 'architecture_str',
                'is_fat', 'architecture_count', 'architectures', 'architecture_info',
                'analysis_date'
            ]

            column_type_names = [
                'FixedString(64)', 'FixedString(32)', 'FixedString(40)',
                'Nullable(FixedString(64))', 'Nullable(UInt32)', 'LowCardinality(Nullable(String))',
                'UInt8', 'UInt32', 'Array(LowCardinality(String))', 'JSON',
                'DateTime64(3, \'UTC\')'
            ]

            return (data, column_names, column_type_names)

        return None

    def prepare_fat_architecture_export_data(self) -> Any:
        """Prepare export data for the FAT binary architecture mapping table."""
        mappings = self._extract_fat_architecture_mappings()
        if not mappings:
            return None

        data = []
        for mapping in mappings:
            data.append([
                mapping['fat_hash'],
                mapping['architecture'],
                mapping['arch_sha256'],
                mapping['arch_md5'],
                mapping['arch_sha1'],
                mapping['arch_filename'],
                mapping['analysis_date'],
            ])

        column_names = [
            'fat_hash', 'architecture', 'arch_sha256', 'arch_md5', 'arch_sha1',
            'arch_filename', 'analysis_date'
        ]

        column_type_names = [
            'FixedString(64)', 'LowCardinality(String)', 'FixedString(64)',
            'FixedString(32)', 'FixedString(40)', 'String',
            'DateTime64(3, \'UTC\')'
        ]

        return (data, column_names, column_type_names)

    def get_clickhouse_table(self) -> str:
        return "redb_macho_universal"

    # def get_fat_architecture_table(self) -> str:
    #     """Return table name for FAT binary architecture mappings."""
    #     return "redb_fat_binary_architectures"