דף הפרטים הטכניים של השקיפות בינארית של Pixel

ביומן Pixel Binary Transparency Log המערכת משתמשת בטכנולוגיה של יומן שקיפות.

השימוש ביומני שקיפות הוכח באמצעות Certificate Transparency – שקיפות באינטרנט פרוטוקול שדורש מרשויות האישורים לפרסם את האישורים שהן משתמשות בו בעיה ביומנים ציבוריים של שקיפות אישורים. התהליך הזה הצטמצם מאוד הנפקת אישורים שגויה, ובכך משפרת את האבטחה אינטרנט. אופרטורים רבים של יומן שקיפות אישורים מסתמכים על הטמעה מיומני השקיפות שנמצאים ב-transparency.dev.

יומני שקיפות מוטמעים עם עצי Merkle. הדף הזה מבוסס על ההנחה ידע על עצי מרקל ושקיפות בינארית. צפייה מבני נתונים ניתנים לאימות לקבלת סקירה כללית על עצי מרקל בדף הנחיתה לסקירה כללית של קובץ בינארי במידה הולמת.

הטמעת יומנים

יומן השקיפות של Pixel Binary הוטמע בתור עץ מרקל מבוסס-אריחים. הרמה הבסיסית (root) מתוכן המשבצות https://developers.google.com/android/binary_transparency/tile. הערה: מדובר לא דף אינטרנט רגיל. הרשומות ביומן שכלולות בספריות המשנה שלו להיות קריאה פרוגרמטית באמצעות Golang SumDB ספריית TLog ולא באמצעות בדפדפן.

בקטע תוכן היומן אפשר לתיאור של התוכן שמכיל את הרשומות.

גיבוב השורש של עץ Merkle של יומן, שכלול בנקודת ביקורת, מוצג https://developers.google.com/android/binary_transparency/checkpoint.txt. הוא מוצג פורמט נקודת ביקורת (checkpoint). העלים של עץ Merkle זה מוגשים בכתובת https://developers.google.com/android/binary_transparency/image_info.txt. אפשר לאמת את החתימה של נקודת הביקורת באמצעות המפתח הציבורי הבא:

תהליך האימות קורא את נקודת הביקורת ואת כרטיסי המידע שמכיל את הרשומות ביומן.

תהליך האימות

יומן שקיפות מוטמע עם עץ Merkle שמורכב מגיבובים. א' צומת עלה מכיל נתונים, וצומת הורה מכיל את הגיבוב של הצאצאים שלו.

מתבצעות שתי חישובים בעץ ה-Merkle כדי לאמת את הנגיעה המאפיין של יומני שקיפות: ההוכחה להכללה והוכחת העקביות. קודם מוכיח שהיומן כולל רשומה שתואמת לגרסת תמונה, כלומר. הרשומה ביומן כוללת את VBMeta לתגובה, גיבוב (hash) שמייצג את התמונות של מערכת ההפעלה, שאפשר להחזיר מהמכשיר. השנייה מוכיחה שכשמתווספות רשומות חדשות לעץ, נקודת הביקורת החדשה בהתאם לגרסה הקודמת של העץ.

כדי לאמת את תמונת ה-Pixel, יש לשלוח את הוכחת ההכללה. ביצוע לא חובה לבצע חישובים של הוכחת עקביות, כי צדדים שלישיים עשינו זאת.

אם אתם רוצים להכיר את מושגי האימות ב-Pixel אם יש לכם שקיפות בינארית, תוכלו לפעול לפי ההוראות הבאות כדי להשתמש בתמונה פועלת במכשיר Pixel. אם רוצים להריץ את הקושחה של Pixel עם רמת הטעינה הגבוהה ביותר ברמת המהימנות, אפשר לעיין בתהליך האימות אימות מלא של Pixel Binary Transparency

דרישות מוקדמות

מוודאים שיחסי התלות הבאים זמינים:

Golang: צריך ליצור את כלי האימות עם Go 1.17 ואילך, זמין באתר של Go.
Android Debug Bridge (adb): מתקשר עם מכשיר Android לצורך בדיקה את התמונה, שזמינה אתר הכלים של Android SDK.
מאמת הכללה: ממשק עם היומן כדי לבדוק שמכשיר Pixel התמונה נמצאת ביומן השקיפות הבינארי.

# Source code for the inclusion proof verifier is found at avb/tools/transparency/verify
git clone https://android.googlesource.com/platform/external/avb

הוכחה להכללה

בעלים של Pixel יכול לבדוק שהתמונה שלו ביומן על ידי חילוץ של מטא-נתונים רלוונטיים, ולאחר מכן משווים את גיבוב השורש המחושב מחדש שלהם לגיבוב השורש. במסגרת נקודת ביקורת שפורסמה. אם הם תואמים, הבעלים של מכשיר Pixel יכול להבטיח הגנות מסוימות דרך הדוגמה מודל איומים.

כדי לבדוק שהתמונה במכשיר Pixel נמצאת ביומן השקיפות, מתחברים למכשיר באמצעות adb, ולאחר מכן מריצים את הפקודות הבאות:

FINGERPRINT=$(adb shell getprop ro.build.fingerprint)
VBMETA_DIGEST=$(adb shell getprop ro.boot.vbmeta.digest)
LOG_ENTRY="${FINGERPRINT}\n${VBMETA_DIGEST}\n"
PAYLOAD_PATH="/tmp/log_payload.txt"
echo -e $LOG_ENTRY >> $PAYLOAD_PATH

cd avb/tools/transparency/verify/
go build cmd/verifier/verifier.go
./verifier --payload_path=$PAYLOAD_PATH

הבית הראשון מאחזרת את המטא-נתונים ממכשיר Pixel בפורמט של רשומה ביומן, ושומרת אותה ב-/tmp/log_payload.txt.

הבית השני מפעיל את מאמת ההכללה שפורסם מאגר ההפעלה של Android Verified. הכלי הזה מחשב את הגיבוב של רשומת המועמד ביומן, ומאחזר את הפרטים האחרים גיבובים (hash) הנדרשים כדי לחשב מחדש את נקודת הביקורת מהיומן, ומשווה אותה את נקודת הביקורת שמתפרסם על ידי היומן.

הפלט של הפקודה נכתב ל-stdout:

OK אם התמונה נכללת ביומן,
FAILURE אם לא.

הוכחה לעקביות (אופציונלי)

מכיוון ש-Google מפרסמת מדי פעם גרסאות חדשות של תמונת היצרן של Pixel, יומן השקיפות גדל כל הזמן. עד בודק שהעץ צומח באופן שתואם העלים הקודמים שלו. העד עוקב אחר גיבוב (hash) של שורש עץ, ומחשב את גיבוב השורש של המועמד הבא על ידי בקשת הערך החדש עלים מגובבים (hashed) מהעץ. כדי שיומן שקיפות יהיה ברור, עליו את העקביות בנתונים.

התנהגות ההוספה בלבד של יומן השקיפות נבדקת באופן פעיל על ידי צד שלישי ולכן רוב המשתמשים לא צריכים לעשות זאת בעצמם, אבל ייתכן כדי שכולם יוכלו לעקוב אחרי העקביות של היומן. Google פרסמה מאמר קוד פתוח של עדות מאגר GitHub. צריך להשתמש הגדרה ספציפי ליומן של Pixel Binary Transparency (PixelBT).